![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > elexd | Unicode version |
Description: If a class is a member of another class, it is a set. (Contributed by Glauco Siliprandi, 11-Oct-2020.) |
Ref | Expression |
---|---|
elexd.1 |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Ref | Expression |
---|---|
elexd |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | elexd.1 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
2 | elex 2748 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
3 | 1, 2 | syl 14 |
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 1447 ax-gen 1449 ax-ie1 1493 ax-ie2 1494 ax-8 1504 ax-4 1510 ax-17 1526 ax-i9 1530 ax-ial 1534 ax-ext 2159 |
This theorem depends on definitions: df-bi 117 df-sb 1763 df-clab 2164 df-cleq 2170 df-clel 2173 df-v 2739 |
This theorem is referenced by: ifexd 4480 dmmptd 5341 tfr1onlemsucfn 6334 tfrcllemsucfn 6347 frecrdg 6402 unsnfidcel 6913 fnfi 6929 caseinl 7083 caseinr 7084 omniwomnimkv 7158 nninfdcinf 7162 acfun 7199 seq3val 10431 seqvalcd 10432 hashennn 10731 lcmval 12033 hashdvds 12191 ennnfonelemp1 12377 isstruct2r 12443 strnfvnd 12452 strfvssn 12454 strslfv2d 12474 setsslid 12482 basmex 12490 basmexd 12491 ressbas2d 12497 ressval3d 12500 ismgmn0 12656 ismhm 12730 0mhm 12750 mulgval 12862 mulgfng 12863 mulg1 12866 mulgnnp1 12867 mulgnndir 12887 issrg 12961 ringidss 13025 ringpropd 13030 dvdsrvald 13074 dvdsrd 13075 isunitd 13087 invrfvald 13103 istopon 13144 istps 13163 tgclb 13198 restbasg 13301 restco 13307 lmfval 13325 cnfval 13327 cnpfval 13328 cnpval 13331 txcnp 13404 txrest 13409 ismet2 13487 xmetpsmet 13502 mopnval 13575 comet 13632 reldvg 13781 dvmptclx 13813 |
Copyright terms: Public domain | W3C validator |