![]() |
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 2763 |
. 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 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: ifexd 4502 dmmptd 5365 tfr1onlemsucfn 6366 tfrcllemsucfn 6379 frecrdg 6434 unsnfidcel 6950 fnfi 6967 caseinl 7121 caseinr 7122 omniwomnimkv 7196 nninfdcinf 7200 acfun 7237 seq3val 10491 seqvalcd 10492 hashennn 10795 lcmval 12098 hashdvds 12256 ennnfonelemp1 12460 isstruct2r 12526 strnfvnd 12535 strfvssn 12537 strslfv2d 12558 setsslid 12566 basmex 12574 basmexd 12575 ressbas2d 12583 ressval3d 12587 prdsex 12777 imasival 12786 imasbas 12787 imasplusg 12788 imasmulr 12789 imasaddfn 12797 imasaddval 12798 imasaddf 12799 imasmulfn 12800 imasmulval 12801 imasmulf 12802 qusval 12803 qusaddflemg 12813 qusaddval 12814 qusaddf 12815 qusmulval 12816 qusmulf 12817 xpsfrnel 12823 xpsval 12831 ismgmn0 12837 igsumvalx 12868 gsumval2 12875 ress0g 12919 ismhm 12928 mhmex 12929 0mhm 12953 qusgrp2 13070 mulgval 13079 mulgfng 13081 mulg1 13086 mulgnnp1 13087 mulgnndir 13108 issubg2m 13145 1nsgtrivd 13175 eqgval 13179 eqgen 13183 rngpropd 13326 qusrng 13329 issrg 13336 ringidss 13400 ringpropd 13409 qusring2 13433 dvdsrvald 13460 dvdsrd 13461 isunitd 13473 invrfvald 13489 dvrfvald 13500 rdivmuldivd 13511 invrpropdg 13516 isrim0 13528 rhmunitinv 13545 subrgintm 13607 aprval 13615 lssmex 13688 islss3 13712 sraval 13770 sralemg 13771 srascag 13775 sravscag 13776 sraipg 13777 sraex 13779 lidlmex 13808 lidlrsppropdg 13828 2idlmex 13835 psrval 13961 psrbasg 13968 psrplusgg 13971 psraddcl 13973 istopon 13990 istps 14009 tgclb 14042 restbasg 14145 restco 14151 lmfval 14169 cnfval 14171 cnpfval 14172 cnpval 14175 txcnp 14248 txrest 14253 ismet2 14331 xmetpsmet 14346 mopnval 14419 comet 14476 reldvg 14625 dvmptclx 14657 lgseisenlem2 14929 |
Copyright terms: Public domain | W3C validator |