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 2671 | . 2 | |
3 | 1, 2 | syl 14 | 1 |
Colors of variables: wff set class |
Syntax hints: wi 4 wcel 1465 cvv 2660 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 105 ax-ia2 106 ax-ia3 107 ax-5 1408 ax-gen 1410 ax-ie1 1454 ax-ie2 1455 ax-8 1467 ax-4 1472 ax-17 1491 ax-i9 1495 ax-ial 1499 ax-ext 2099 |
This theorem depends on definitions: df-bi 116 df-sb 1721 df-clab 2104 df-cleq 2110 df-clel 2113 df-v 2662 |
This theorem is referenced by: dmmptd 5223 tfr1onlemsucfn 6205 tfrcllemsucfn 6218 frecrdg 6273 unsnfidcel 6777 fnfi 6793 caseinl 6944 caseinr 6945 acfun 7031 seq3val 10199 seqvalcd 10200 hashennn 10494 lcmval 11671 hashdvds 11824 ennnfonelemp1 11846 isstruct2r 11897 strnfvnd 11906 strfvssn 11908 strslfv2d 11928 setsslid 11936 ressid2 11945 ressval2 11946 istopon 12107 istps 12126 tgclb 12161 restbasg 12264 restco 12270 lmfval 12288 cnfval 12290 cnpfval 12291 cnpval 12294 txcnp 12367 txrest 12372 ismet2 12450 xmetpsmet 12465 mopnval 12538 comet 12595 reldvg 12744 dvmptclx 12776 |
Copyright terms: Public domain | W3C validator |