ssel2 - Metamath Proof Explorer

Metamath Proof Explorer

< Previous Next >
Related theorems
Unicode version

Theorem ssel2 2054

Description: Membership relationships follow from a subclass relationship.

**Assertion**
Ref	Expression
ssel2	$/\$

**Proof of Theorem ssel2**
Step	Hyp	Ref	Expression
1		ssel 2053	. 2
2	1	imp 350	1 $/\$

Colors of variables: wff set class

Syntax hints:

wi 3 $/\$ wa 223

wcel 955

wss 2037

This theorem is referenced by: tz7.7 2963 onnmin 3005 onmindif 3050 onmindif2 3051 ordunisssuc 3073 limsssuc 3111 ssimaex 3753 1st2nd 4092 fundmen 4409 isfinite2 4523 suplem2pr 5134 axsup 5479 lbinfm 5995 suprleub 6006 dfinfmr 6014 infmrcl 6016 xrsupsslem 6023 xrinfmsslem 6024 xrub 6027 supxr2 6029 supxrre 6030 supxrun 6032 supxrunb1 6036 supxrbnd 6038 supxrbnd1 6042 supxrbnd2 6043 supxrub 6045 supxrleub 6046 uzwo4OLD 6158 shftf 6288 uzwo 6387 uzwoOLD 6388 sumeqfv 6935 infxpidmlem5 7499 infxpidmlem7 7501 infxpidmlem8 7502 tgclt 7566 fctop 7592 cctop 7594 neips 7668 isopn4 7802 opni3 7806 opnuni 7808 lpbl 7819 metcnplem 7825 metelcls 7900 ubthlem11 8470 ocsh 9072 ocorth 9080 spansncv 9514 pjss1co 10002 sumdmdi 10249 efilcp 10445 efilcp2 10450

This theorem was proved from axioms: ax-1 4 ax-2 5 ax-3 6 ax-mp 7 ax-7 959 ax-gen 960 ax-8 961 ax-10 963 ax-12 965 ax-17 968 ax-4 970 ax-5o 972 ax-6o 975 ax-9o 1119 ax-10o 1136 ax-16 1206 ax-11o 1213 ax-ext 1452

This theorem depends on definitions: df-bi 147 df-an 225 df-ex 978 df-sb 1168 df-clab 1457 df-cleq 1462 df-clel 1465 df-in 2041 df-ss 2043