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 2993 | . 2 | |
3 | 1, 2 | ax-mp 7 | 1 |
Colors of variables: wff set class |
Syntax hints: wi 4 wcel 1433 wss 2973 |
This theorem was proved from axioms: ax-1 5 ax-2 6 ax-mp 7 ax-ia1 104 ax-ia2 105 ax-ia3 106 ax-5 1376 ax-7 1377 ax-gen 1378 ax-ie1 1422 ax-ie2 1423 ax-8 1435 ax-11 1437 ax-4 1440 ax-17 1459 ax-i9 1463 ax-ial 1467 ax-i5r 1468 ax-ext 2063 |
This theorem depends on definitions: df-bi 115 df-nf 1390 df-sb 1686 df-clab 2068 df-cleq 2074 df-clel 2077 df-in 2979 df-ss 2986 |
This theorem is referenced by: sselii 2996 sseldi 2997 elun1 3139 elun2 3140 finds 4341 finds2 4342 issref 4727 2elresin 5030 fvun1 5260 fvmptssdm 5276 fvimacnvi 5302 elpreima 5307 ofrfval 5740 fnofval 5741 off 5744 offres 5782 eqopi 5818 op1steq 5825 dfoprab4 5838 f1od2 5876 reldmtpos 5891 smores3 5931 smores2 5932 pinn 6499 indpi 6532 enq0enq 6621 preqlu 6662 elinp 6664 prop 6665 elnp1st2nd 6666 prarloclem5 6690 cauappcvgprlemladd 6848 peano5nnnn 7058 nnindnn 7059 recn 7106 rexr 7164 peano5nni 8042 nnre 8046 nncn 8047 nnind 8055 nnnn0 8295 nn0re 8297 nn0cn 8298 nnz 8370 nn0z 8371 nnq 8718 qcn 8719 rpre 8740 iccshftri 9017 iccshftli 9019 iccdili 9021 icccntri 9023 fzval2 9032 fzelp1 9091 4fvwrd4 9150 elfzo1 9199 expcllem 9487 expcl2lemap 9488 m1expcl2 9498 bcm1k 9687 bcpasc 9693 cau3lem 10000 climconst2 10130 dvdsflip 10251 infssuzcldc 10347 isprm3 10500 |
Copyright terms: Public domain | W3C validator |