![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > eqimss2 | Structured version Visualization version Unicode version |
Description: Equality implies the subclass relation. (Contributed by NM, 23-Nov-2003.) |
Ref | Expression |
---|---|
eqimss2 |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | eqimss 3496 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
2 | 1 | eqcoms 2470 |
1
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Colors of variables: wff setvar class |
Syntax hints: ![]() ![]() ![]() |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1680 ax-4 1693 ax-5 1769 ax-6 1816 ax-7 1862 ax-10 1926 ax-11 1931 ax-12 1944 ax-13 2102 ax-ext 2442 |
This theorem depends on definitions: df-bi 190 df-an 377 df-tru 1458 df-ex 1675 df-nf 1679 df-sb 1809 df-clab 2449 df-cleq 2455 df-clel 2458 df-in 3423 df-ss 3430 |
This theorem is referenced by: disjeq2 4391 disjeq1 4394 poeq2 4778 freq2 4824 seeq1 4825 seeq2 4826 dmcoeq 5116 xp11 5291 suc11 5545 funeq 5620 fconst3 6153 sorpssuni 6607 sorpssint 6608 tposeq 7001 oaass 7288 odi 7306 oen0 7313 inficl 7965 cantnfp1lem1 8209 cantnflem1 8220 fodomfi2 8517 zorng 8960 rlimclim 13659 imasaddfnlem 15483 imasvscafn 15492 gasubg 17005 pgpssslw 17315 dprddisj2 17721 dprd2da 17724 evlslem6 18785 topgele 19998 topontopn 20006 toponmre 20158 conima 20489 islocfin 20581 ptbasfi 20645 txdis 20696 neifil 20944 elfm3 21014 rnelfmlem 21016 alexsubALTlem3 21113 alexsubALTlem4 21114 utopsnneiplem 21311 lmclimf 22322 uniiccdif 22584 dv11cn 23002 plypf1 23215 subgores 26081 hstoh 27934 dmdi2 28006 disjeq1f 28233 eulerpartlemd 29248 rrvdmss 29331 refssfne 31063 neibastop3 31067 topmeet 31069 topjoin 31070 fnemeet2 31072 fnejoin1 31073 heiborlem3 32190 lsatelbN 32617 lkrscss 32709 lshpset2N 32730 mapdrvallem2 35258 hdmaprnlem3eN 35474 hdmaplkr 35529 ssrecnpr 36700 founiiun 37484 founiiun0 37503 caragendifcl 38373 1wlkvtxiedg 39687 wlk1wlk 39699 2pthon3v-av 39892 |
Copyright terms: Public domain | W3C validator |