![]() |
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, then 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 1628 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
2 | df-clel 2185 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
3 | isset 2758 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
4 | 1, 2, 3 | 3imtr4i 201 |
1
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Colors of variables: wff set class |
Syntax hints: ![]() ![]() ![]() ![]() ![]() ![]() |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 106 ax-ia2 107 ax-ia3 108 ax-5 1458 ax-gen 1460 ax-ie1 1504 ax-ie2 1505 ax-8 1515 ax-4 1521 ax-17 1537 ax-i9 1541 ax-ial 1545 ax-ext 2171 |
This theorem depends on definitions: df-bi 117 df-sb 1774 df-clab 2176 df-cleq 2182 df-clel 2185 df-v 2754 |
This theorem is referenced by: elexi 2764 elexd 2765 elisset 2766 vtoclgft 2802 vtoclgf 2810 vtoclg1f 2811 vtocl2gf 2814 vtocl3gf 2815 spcimgft 2828 spcimegft 2830 elab4g 2901 elrabf 2906 mob 2934 sbcex 2986 sbcel1v 3040 sbcabel 3059 csbcomg 3095 csbvarg 3100 csbiebt 3111 csbnestgf 3124 csbidmg 3128 sbcco3g 3129 csbco3g 3130 eldif 3153 ssv 3192 elun 3291 elin 3333 elpwb 3600 snidb 3637 snssg 3741 dfopg 3791 eluni 3827 eliun 3905 csbexga 4146 nvel 4151 class2seteq 4181 axpweq 4189 snelpwi 4230 opexg 4246 elopab 4276 epelg 4308 elon2 4394 unexg 4461 reuhypd 4489 sucexg 4515 onsucb 4520 onsucelsucr 4525 sucunielr 4527 en2lp 4571 peano2 4612 peano2b 4632 opelvvg 4693 opeliunxp 4699 opeliunxp2 4785 ideqg 4796 elrnmptg 4897 imasng 5011 iniseg 5018 opswapg 5133 elxp4 5134 elxp5 5135 dmmptg 5144 iota2 5225 fnmpt 5361 fvexg 5553 fvelimab 5593 mptfvex 5622 fvmptdf 5624 fvmptdv2 5626 mpteqb 5627 fvmptt 5628 fvmptf 5629 fvopab6 5633 fsn2 5711 fmptpr 5729 eloprabga 5983 ovmpos 6020 ov2gf 6021 ovmpodxf 6022 ovmpox 6025 ovmpoga 6026 ovmpodf 6028 ovi3 6033 ovelrn 6045 suppssfv 6102 suppssov1 6103 offval3 6159 1stexg 6192 2ndexg 6193 elxp6 6194 elxp7 6195 releldm2 6210 fnmpo 6227 mpofvex 6228 mpoexg 6236 opeliunxp2f 6263 brtpos2 6276 rdgtfr 6399 rdgruledefgg 6400 frec0g 6422 sucinc2 6471 nntri3or 6518 relelec 6601 ecdmn0m 6603 mapvalg 6684 pmvalg 6685 elpmg 6690 elixp2 6728 mptelixpg 6760 elixpsn 6761 map1 6838 mapdom1g 6875 mapxpen 6876 fival 6999 elfi2 7001 djulclr 7078 djurclr 7079 djulcl 7080 djurcl 7081 djulclb 7084 inl11 7094 djuss 7099 1stinl 7103 2ndinl 7104 1stinr 7105 2ndinr 7106 ismkvnex 7183 omniwomnimkv 7195 cc4n 7300 elinp 7503 addnqprlemfl 7588 addnqprlemfu 7589 mulnqprlemfl 7604 mulnqprlemfu 7605 recexprlemell 7651 recexprlemelu 7652 shftfvalg 10859 clim 11321 climmpt 11340 climshft2 11346 4sqlem2 12421 isstruct2r 12523 slotex 12539 setsvalg 12542 setsfun0 12548 setscom 12552 ressvalsets 12576 ressbasid 12582 restval 12750 topnvalg 12756 tgval 12767 ptex 12769 prdsex 12774 imasex 12782 qusex 12802 qusaddvallemg 12809 xpsfrnel2 12822 plusffvalg 12838 grpidvalg 12849 sgrp1 12874 issubmnd 12903 issubm 12924 grppropstrg 12964 grpinvfvalg 12986 grpinvfng 12988 grpsubfvalg 12989 grpressid 13005 mulgfvalg 13063 mulgex 13065 mulgfng 13066 issubg 13112 subgex 13115 releqgg 13159 eqgex 13160 eqgfval 13161 isghm 13182 ablressid 13272 mgpvalg 13277 mgptopng 13283 rngressid 13308 rngpropd 13309 ringidvalg 13315 dfur2g 13316 issrg 13319 iscrng2 13369 ringressid 13413 opprvalg 13419 reldvdsrsrg 13442 dvdsrex 13448 unitgrp 13466 unitabl 13467 unitlinv 13476 unitrinv 13477 issubrng 13546 issubrg 13568 subrgugrp 13587 aprap 13602 islmod 13607 scaffvalg 13622 lsssetm 13672 islssmg 13674 lspfval 13704 lspval 13706 lspcl 13707 lspex 13711 sraval 13753 rlmvalg 13770 rlmsubg 13774 rlmvnegg 13781 ixpsnbasval 13782 lidlvalg 13787 rspvalg 13788 lidlex 13789 rspex 13790 2idlvalg 13817 zrhvalg 13915 zlmval 13923 toponsspwpwg 13979 eltg 14009 eltg2 14010 restbasg 14125 tgrest 14126 txvalex 14211 txval 14212 ispsmet 14280 ismet 14301 isxmet 14302 xmetunirn 14315 blfvalps 14342 bj-vtoclgft 14985 djucllem 15010 bj-nvel 15107 |
Copyright terms: Public domain | W3C validator |