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 2939 | . 2 | |
3 | 1, 2 | ax-mp 7 | 1 |
Colors of variables: wff set class |
Syntax hints: wi 4 wcel 1393 wss 2917 |
This theorem was proved from axioms: ax-1 5 ax-2 6 ax-mp 7 ax-ia1 99 ax-ia2 100 ax-ia3 101 ax-5 1336 ax-7 1337 ax-gen 1338 ax-ie1 1382 ax-ie2 1383 ax-8 1395 ax-11 1397 ax-4 1400 ax-17 1419 ax-i9 1423 ax-ial 1427 ax-i5r 1428 ax-ext 2022 |
This theorem depends on definitions: df-bi 110 df-nf 1350 df-sb 1646 df-clab 2027 df-cleq 2033 df-clel 2036 df-in 2924 df-ss 2931 |
This theorem is referenced by: sselii 2942 sseldi 2943 elun1 3110 elun2 3111 finds 4323 finds2 4324 issref 4707 2elresin 5010 fvun1 5239 fvmptssdm 5255 fvimacnvi 5281 elpreima 5286 ofrfval 5720 fnofval 5721 off 5724 offres 5762 eqopi 5798 op1steq 5805 dfoprab4 5818 reldmtpos 5868 smores3 5908 smores2 5909 pinn 6407 indpi 6440 enq0enq 6529 preqlu 6570 elinp 6572 prop 6573 elnp1st2nd 6574 prarloclem5 6598 cauappcvgprlemladd 6756 peano5nnnn 6966 nnindnn 6967 recn 7014 rexr 7071 peano5nni 7917 nnre 7921 nncn 7922 nnind 7930 nnnn0 8188 nn0re 8190 nn0cn 8191 nnz 8264 nn0z 8265 nnq 8568 qcn 8569 rpre 8589 iccshftri 8863 iccshftli 8865 iccdili 8867 icccntri 8869 fzval2 8877 fzelp1 8936 4fvwrd4 8997 elfzo1 9046 expcllem 9266 expcl2lemap 9267 m1expcl2 9277 cau3lem 9710 climconst2 9812 |
Copyright terms: Public domain | W3C validator |