sselid - Intuitionistic Logic Explorer

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

Theorem sselid 3140

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 3138	. 2
4	1, 3	syl 14	1

Colors of variables: wff set class

Syntax hints:

wi 4

wcel 2136

wss 3116

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 1435 ax-7 1436 ax-gen 1437 ax-ie1 1481 ax-ie2 1482 ax-8 1492 ax-11 1494 ax-4 1498 ax-17 1514 ax-i9 1518 ax-ial 1522 ax-i5r 1523 ax-ext 2147

This theorem depends on definitions: df-bi 116 df-nf 1449 df-sb 1751 df-clab 2152 df-cleq 2158 df-clel 2161 df-in 3122 df-ss 3129

This theorem is referenced by: mptrcl 5568 riotacl 5812 riotasbc 5813 elmpocl 6036 ofrval 6060 f1od2 6203 mpoxopn0yelv 6207 tpostpos 6232 smores 6260 supubti 6964 suplubti 6965 prarloclemcalc 7443 rereceu 7830 recriota 7831 rexrd 7948 eqord1 8381 nnred 8870 nncnd 8871 un0addcl 9147 un0mulcl 9148 nnnn0d 9167 nn0red 9168 nn0xnn0d 9186 suprzclex 9289 nn0zd 9311 zred 9313 rpred 9632 ige2m1fz 10045 zmodfzp1 10283 seq3caopr2 10417 expcl2lemap 10467 m1expcl 10478 summodclem2a 11322 zsumdc 11325 clim2prod 11480 ntrivcvgap 11489 prodmodclem2a 11517 zproddc 11520 zsupssdc 11887 lcmn0cl 12000 isprm5lem 12073 eulerthlemrprm 12161 eulerthlema 12162 eulerthlemh 12163 eulerthlemth 12164 prmdivdiv 12169 ennnfonelemg 12336 lmrcl 12831 lmss 12886 upxp 12912 isxms2 13092 iooretopg 13168 tgqioo 13187 limccoap 13287 dvcl 13292 dvidlemap 13300 dvcnp2cntop 13303 lgscl 13555 2sqlem6 13596 2sqlem8 13599 2sqlem9 13600 isomninnlem 13909 trilpolemeq1 13919 trilpolemlt1 13920 iswomninnlem 13928 iswomni0 13930 ismkvnnlem 13931 nconstwlpolemgt0 13942