![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > eqimss2 | Structured version Visualization version GIF version |
Description: Equality implies the subclass relation. (Contributed by NM, 23-Nov-2003.) |
Ref | Expression |
---|---|
eqimss2 | ⊢ (𝐵 = 𝐴 → 𝐴 ⊆ 𝐵) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | eqimss 3806 | . 2 ⊢ (𝐴 = 𝐵 → 𝐴 ⊆ 𝐵) | |
2 | 1 | eqcoms 2779 | 1 ⊢ (𝐵 = 𝐴 → 𝐴 ⊆ 𝐵) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 = wceq 1631 ⊆ wss 3723 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1870 ax-4 1885 ax-5 1991 ax-6 2057 ax-7 2093 ax-9 2154 ax-10 2174 ax-11 2190 ax-12 2203 ax-ext 2751 |
This theorem depends on definitions: df-bi 197 df-an 383 df-or 837 df-tru 1634 df-ex 1853 df-nf 1858 df-sb 2050 df-clab 2758 df-cleq 2764 df-clel 2767 df-in 3730 df-ss 3737 |
This theorem is referenced by: ifpprsnss 4436 disjeq2 4759 disjeq1 4762 poeq2 5175 freq2 5221 seeq1 5222 seeq2 5223 dmcoeq 5525 xp11 5709 suc11 5973 funeq 6050 fconst3 6623 sorpssuni 7096 sorpssint 7097 tposeq 7509 oaass 7798 odi 7816 oen0 7823 inficl 8490 cantnfp1lem1 8742 cantnflem1 8753 fodomfi2 9086 zorng 9531 rlimclim 14484 imasaddfnlem 16395 imasvscafn 16404 gasubg 17941 pgpssslw 18235 dprddisj2 18645 dprd2da 18648 evlslem6 19727 topgele 20954 topontopn 20964 toponmre 21117 connima 21448 islocfin 21540 ptbasfi 21604 txdis 21655 neifil 21903 elfm3 21973 rnelfmlem 21975 alexsubALTlem3 22072 alexsubALTlem4 22073 utopsnneiplem 22270 lmclimf 23320 uniiccdif 23565 dv11cn 23983 plypf1 24187 2pthon3v 27089 hstoh 29430 dmdi2 29502 disjeq1f 29724 eulerpartlemd 30767 rrvdmss 30850 refssfne 32689 neibastop3 32693 topmeet 32695 topjoin 32696 fnemeet2 32698 fnejoin1 32699 bj-restuni 33381 heiborlem3 33943 lsatelbN 34814 lkrscss 34906 lshpset2N 34927 mapdrvallem2 37455 hdmaprnlem3eN 37668 hdmaplkr 37723 uneqsn 38847 ssrecnpr 39033 founiiun 39879 founiiun0 39896 caragendifcl 41245 |
Copyright terms: Public domain | W3C validator |