Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > ILE Home > Th. List > sseli | Unicode version |
Description: Membership inference from subclass relationship. (Contributed by NM, 5-Aug-1993.) |
Ref | Expression |
---|---|
sseli.1 |
Ref | Expression |
---|---|
sseli |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | sseli.1 | . 2 | |
2 | ssel 3061 | . 2 | |
3 | 1, 2 | ax-mp 5 | 1 |
Colors of variables: wff set class |
Syntax hints: wi 4 wcel 1465 wss 3041 |
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 1408 ax-7 1409 ax-gen 1410 ax-ie1 1454 ax-ie2 1455 ax-8 1467 ax-11 1469 ax-4 1472 ax-17 1491 ax-i9 1495 ax-ial 1499 ax-i5r 1500 ax-ext 2099 |
This theorem depends on definitions: df-bi 116 df-nf 1422 df-sb 1721 df-clab 2104 df-cleq 2110 df-clel 2113 df-in 3047 df-ss 3054 |
This theorem is referenced by: sselii 3064 sseldi 3065 elun1 3213 elun2 3214 finds 4484 finds2 4485 issref 4891 2elresin 5204 fvun1 5455 fvmptssdm 5473 elfvmptrab1 5483 fvimacnvi 5502 elpreima 5507 ofrfval 5958 ofvalg 5959 off 5962 offres 6001 eqopi 6038 op1steq 6045 dfoprab4 6058 f1od2 6100 reldmtpos 6118 smores3 6158 smores2 6159 ctssdccl 6964 pinn 7085 indpi 7118 enq0enq 7207 preqlu 7248 elinp 7250 prop 7251 elnp1st2nd 7252 prarloclem5 7276 cauappcvgprlemladd 7434 peano5nnnn 7668 nnindnn 7669 recn 7721 rexr 7779 peano5nni 8691 nnre 8695 nncn 8696 nnind 8704 nnnn0 8952 nn0re 8954 nn0cn 8955 nn0xnn0 9012 nnz 9041 nn0z 9042 nnq 9393 qcn 9394 rpre 9416 iccshftri 9746 iccshftli 9748 iccdili 9750 icccntri 9752 fzval2 9761 fzelp1 9822 4fvwrd4 9885 elfzo1 9935 expcllem 10272 expcl2lemap 10273 m1expcl2 10283 bcm1k 10474 bcpasc 10480 cau3lem 10854 climconst2 11028 fsum3 11124 binomlem 11220 cos12dec 11401 dvdsflip 11476 infssuzcldc 11571 isprm3 11726 phimullem 11828 structcnvcnv 11902 fvsetsid 11920 tgval2 12147 qtopbasss 12617 dedekindicc 12707 ivthinc 12717 ivthdec 12718 cosz12 12788 exmidsbthrlem 13144 |
Copyright terms: Public domain | W3C validator |