Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > ILE Home > Th. List > sseldi | Unicode version |
Description: Membership inference from subclass relationship. (Contributed by NM, 25-Jun-2014.) |
Ref | Expression |
---|---|
sseli.1 | |
sseldi.2 |
Ref | Expression |
---|---|
sseldi |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | sseldi.2 | . 2 | |
2 | sseli.1 | . . 3 | |
3 | 2 | sseli 3093 | . 2 |
4 | 1, 3 | syl 14 | 1 |
Colors of variables: wff set class |
Syntax hints: wi 4 wcel 1480 wss 3071 |
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 1423 ax-7 1424 ax-gen 1425 ax-ie1 1469 ax-ie2 1470 ax-8 1482 ax-11 1484 ax-4 1487 ax-17 1506 ax-i9 1510 ax-ial 1514 ax-i5r 1515 ax-ext 2121 |
This theorem depends on definitions: df-bi 116 df-nf 1437 df-sb 1736 df-clab 2126 df-cleq 2132 df-clel 2135 df-in 3077 df-ss 3084 |
This theorem is referenced by: mptrcl 5503 riotacl 5744 riotasbc 5745 elmpocl 5968 ofrval 5992 f1od2 6132 mpoxopn0yelv 6136 tpostpos 6161 smores 6189 supubti 6886 suplubti 6887 prarloclemcalc 7310 rereceu 7697 recriota 7698 rexrd 7815 eqord1 8245 nnred 8733 nncnd 8734 un0addcl 9010 un0mulcl 9011 nnnn0d 9030 nn0red 9031 nn0xnn0d 9049 suprzclex 9149 nn0zd 9171 zred 9173 rpred 9483 ige2m1fz 9890 zmodfzp1 10121 seq3caopr2 10255 expcl2lemap 10305 m1expcl 10316 summodclem2a 11150 zsumdc 11153 clim2prod 11308 ntrivcvgap 11317 prodmodclem2a 11345 lcmn0cl 11749 ennnfonelemg 11916 lmrcl 12360 lmss 12415 upxp 12441 isxms2 12621 iooretopg 12697 tgqioo 12716 limccoap 12816 dvcl 12821 dvidlemap 12829 dvcnp2cntop 12832 isomninnlem 13225 trilpolemeq1 13233 trilpolemlt1 13234 |
Copyright terms: Public domain | W3C validator |