sselid - Intuitionistic Logic Explorer

	Intuitionistic Logic Explorer		< Previous Next > Nearby theorems
Mirrors > Home > ILE Home > Th. List > sselid		Unicode version

Theorem sselid 3145

Description: Membership inference from subclass relationship. (Contributed by NM, 25-Jun-2014.)

**Hypotheses**
Ref	Expression
sseli.1
sselid.2

**Assertion**
Ref	Expression
sselid

**Proof of Theorem sselid**
Step	Hyp	Ref	Expression
1		sselid.2	. 2
2		sseli.1	. . 3
3	2	sseli 3143	. 2
4	1, 3	syl 14	1

Colors of variables: wff set class

Syntax hints:

wi 4

wcel 2141

wss 3121

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 105 ax-ia2 106 ax-ia3 107 ax-5 1440 ax-7 1441 ax-gen 1442 ax-ie1 1486 ax-ie2 1487 ax-8 1497 ax-11 1499 ax-4 1503 ax-17 1519 ax-i9 1523 ax-ial 1527 ax-i5r 1528 ax-ext 2152

This theorem depends on definitions: df-bi 116 df-nf 1454 df-sb 1756 df-clab 2157 df-cleq 2163 df-clel 2166 df-in 3127 df-ss 3134

This theorem is referenced by: mptrcl 5576 riotacl 5821 riotasbc 5822 elmpocl 6045 ofrval 6069 f1od2 6212 mpoxopn0yelv 6216 tpostpos 6241 smores 6269 supubti 6973 suplubti 6974 prarloclemcalc 7453 rereceu 7840 recriota 7841 rexrd 7958 eqord1 8391 nnred 8880 nncnd 8881 un0addcl 9157 un0mulcl 9158 nnnn0d 9177 nn0red 9178 nn0xnn0d 9196 suprzclex 9299 nn0zd 9321 zred 9323 rpred 9642 ige2m1fz 10055 zmodfzp1 10293 seq3caopr2 10427 expcl2lemap 10477 m1expcl 10488 summodclem2a 11333 zsumdc 11336 clim2prod 11491 ntrivcvgap 11500 prodmodclem2a 11528 zproddc 11531 zsupssdc 11898 lcmn0cl 12011 isprm5lem 12084 eulerthlemrprm 12172 eulerthlema 12173 eulerthlemh 12174 eulerthlemth 12175 prmdivdiv 12180 ennnfonelemg 12347 lmrcl 12946 lmss 13001 upxp 13027 isxms2 13207 iooretopg 13283 tgqioo 13302 limccoap 13402 dvcl 13407 dvidlemap 13415 dvcnp2cntop 13418 lgscl 13670 2sqlem6 13711 2sqlem8 13714 2sqlem9 13715 isomninnlem 14024 trilpolemeq1 14034 trilpolemlt1 14035 iswomninnlem 14043 iswomni0 14045 ismkvnnlem 14046 nconstwlpolemgt0 14057