![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > elex | Unicode version |
Description: If a class is a member of another class, it is a set. Theorem 6.12 of [Quine] p. 44. (Contributed by NM, 5-Aug-1993.) (Proof shortened by Andrew Salmon, 8-Jun-2011.) |
Ref | Expression |
---|---|
elex |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | exsimpl 1505 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
2 | df-clel 2033 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
3 | isset 2555 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
4 | 1, 2, 3 | 3imtr4i 190 |
1
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Colors of variables: wff set class |
Syntax hints: ![]() ![]() ![]() ![]() ![]() ![]() |
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 1333 ax-gen 1335 ax-ie1 1379 ax-ie2 1380 ax-8 1392 ax-4 1397 ax-17 1416 ax-i9 1420 ax-ial 1424 ax-ext 2019 |
This theorem depends on definitions: df-bi 110 df-sb 1643 df-clab 2024 df-cleq 2030 df-clel 2033 df-v 2553 |
This theorem is referenced by: elexi 2561 elisset 2562 vtoclgft 2598 vtoclgf 2606 vtocl2gf 2609 vtocl3gf 2610 spcimgft 2623 spcimegft 2625 elab4g 2685 elrabf 2690 mob 2717 sbcex 2766 sbcabel 2833 csbcomg 2867 csbvarg 2871 csbiebt 2880 csbnestgf 2892 csbidmg 2896 sbcco3g 2897 csbco3g 2898 eldif 2921 ssv 2959 elun 3078 elin 3120 snidb 3393 dfopg 3538 eluni 3574 eliun 3652 csbexga 3876 nvel 3880 class2seteq 3907 axpweq 3915 snelpwi 3939 prelpwi 3941 opexg 3955 elopab 3986 epelg 4018 elon2 4079 unexg 4144 reuhypd 4169 op1stbg 4176 sucexg 4190 sucelon 4195 onsucelsucr 4199 sucunielr 4201 en2lp 4232 peano2 4261 peano2b 4280 opelvvg 4332 opeliunxp 4338 opbrop 4362 opeliunxp2 4419 ideqg 4430 elrnmptg 4529 imasng 4633 iniseg 4640 opswapg 4750 elxp4 4751 elxp5 4752 dmmptg 4761 iota2 4836 fnmpt 4968 fvexg 5137 fvelimab 5172 mptfvex 5199 fvmptdf 5201 fvmptdv2 5203 mpteqb 5204 fvmptt 5205 fvmptf 5206 fvopab6 5207 fsn2 5280 fmptpr 5298 fliftel 5376 eloprabga 5533 ovmpt2s 5566 ov2gf 5567 ovmpt2dxf 5568 ovmpt2x 5571 ovmpt2ga 5572 ovmpt2df 5574 ovi3 5579 ovelrn 5591 suppssfv 5650 suppssov1 5651 offval3 5703 1stexg 5736 2ndexg 5737 elxp6 5738 elxp7 5739 releldm2 5753 fnmpt2 5770 mpt2fvex 5771 mpt2exg 5776 brtpos2 5807 rdgtfr 5901 rdgruledefgg 5902 frec0g 5922 sucinc2 5965 nntri3or 6011 relelec 6082 ecdmn0m 6084 elinp 6457 addnqprlemfl 6540 addnqprlemfu 6541 recexprlemell 6594 recexprlemelu 6595 bj-vtoclgft 9249 bj-nvel 9352 |
Copyright terms: Public domain | W3C validator |