![]() |
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 1579 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
2 | df-clel 2111 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
3 | isset 2663 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
4 | 1, 2, 3 | 3imtr4i 200 |
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 105 ax-ia2 106 ax-ia3 107 ax-5 1406 ax-gen 1408 ax-ie1 1452 ax-ie2 1453 ax-8 1465 ax-4 1470 ax-17 1489 ax-i9 1493 ax-ial 1497 ax-ext 2097 |
This theorem depends on definitions: df-bi 116 df-sb 1719 df-clab 2102 df-cleq 2108 df-clel 2111 df-v 2659 |
This theorem is referenced by: elexi 2669 elexd 2670 elisset 2671 vtoclgft 2707 vtoclgf 2715 vtoclg1f 2716 vtocl2gf 2719 vtocl3gf 2720 spcimgft 2733 spcimegft 2735 elab4g 2802 elrabf 2807 mob 2835 sbcex 2886 sbcel1v 2939 sbcabel 2958 csbcomg 2992 csbvarg 2996 csbiebt 3005 csbnestgf 3018 csbidmg 3022 sbcco3g 3023 csbco3g 3024 eldif 3046 ssv 3085 elun 3183 elin 3225 elpwb 3486 snidb 3521 dfopg 3669 eluni 3705 eliun 3783 csbexga 4016 nvel 4021 class2seteq 4047 axpweq 4055 snelpwi 4094 opexg 4110 elopab 4140 epelg 4172 elon2 4258 unexg 4324 reuhypd 4352 sucexg 4374 sucelon 4379 onsucelsucr 4384 sucunielr 4386 en2lp 4429 peano2 4469 peano2b 4488 opelvvg 4548 opeliunxp 4554 opeliunxp2 4639 ideqg 4650 elrnmptg 4751 imasng 4862 iniseg 4869 opswapg 4983 elxp4 4984 elxp5 4985 dmmptg 4994 iota2 5072 fnmpt 5207 fvexg 5394 fvelimab 5431 mptfvex 5460 fvmptdf 5462 fvmptdv2 5464 mpteqb 5465 fvmptt 5466 fvmptf 5467 fvopab6 5471 fsn2 5548 fmptpr 5566 eloprabga 5812 ovmpos 5848 ov2gf 5849 ovmpodxf 5850 ovmpox 5853 ovmpoga 5854 ovmpodf 5856 ovi3 5861 ovelrn 5873 suppssfv 5932 suppssov1 5933 offval3 5986 1stexg 6019 2ndexg 6020 elxp6 6021 elxp7 6022 releldm2 6037 fnmpo 6054 mpofvex 6055 mpoexg 6063 opeliunxp2f 6089 brtpos2 6102 rdgtfr 6225 rdgruledefgg 6226 frec0g 6248 sucinc2 6296 nntri3or 6343 relelec 6423 ecdmn0m 6425 mapvalg 6506 pmvalg 6507 elpmg 6512 elixp2 6550 mptelixpg 6582 elixpsn 6583 map1 6660 mapdom1g 6694 mapxpen 6695 fival 6810 elfi2 6812 djulclr 6886 djurclr 6887 djulcl 6888 djurcl 6889 djulclb 6892 inl11 6902 djuss 6907 1stinl 6911 2ndinl 6912 1stinr 6913 2ndinr 6914 ismkvnex 6979 elinp 7230 addnqprlemfl 7315 addnqprlemfu 7316 mulnqprlemfl 7331 mulnqprlemfu 7332 recexprlemell 7378 recexprlemelu 7379 shftfvalg 10483 clim 10942 climmpt 10961 climshft2 10967 isstruct2r 11813 slotex 11829 setsvalg 11832 setsfun0 11838 setscom 11842 restval 11969 topnvalg 11975 toponsspwpwg 12032 tgval 12061 eltg 12064 eltg2 12065 restbasg 12180 tgrest 12181 txvalex 12265 txval 12266 ispsmet 12312 ismet 12333 isxmet 12334 xmetunirn 12347 blfvalps 12374 bj-vtoclgft 12674 djucllem 12699 bj-nvel 12787 |
Copyright terms: Public domain | W3C validator |