![]() |
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 3913 | . 2 ⊢ (𝐴 = 𝐵 → 𝐴 ⊆ 𝐵) | |
2 | 1 | eqcoms 2786 | 1 ⊢ (𝐵 = 𝐴 → 𝐴 ⊆ 𝐵) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 = wceq 1507 ⊆ wss 3829 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1758 ax-4 1772 ax-5 1869 ax-6 1928 ax-7 1965 ax-8 2052 ax-9 2059 ax-10 2079 ax-11 2093 ax-12 2106 ax-ext 2750 |
This theorem depends on definitions: df-bi 199 df-an 388 df-or 834 df-tru 1510 df-ex 1743 df-nf 1747 df-sb 2016 df-clab 2759 df-cleq 2771 df-clel 2846 df-in 3836 df-ss 3843 |
This theorem is referenced by: ifpprsnss 4574 disjeq2 4901 disjeq1 4904 poeq2 5330 freq2 5378 seeq1 5379 seeq2 5380 dmcoeq 5687 xp11 5872 suc11 6132 funeq 6208 fimadmfoALT 6430 fconst3 6802 sorpssuni 7276 sorpssint 7277 tposeq 7697 oaass 7988 odi 8006 oen0 8013 inficl 8684 fodomfi2 9280 zorng 9724 rlimclim 14764 imasaddfnlem 16657 imasvscafn 16666 gasubg 18203 pgpssslw 18500 dprddisj2 18911 dprd2da 18914 evlslem6 20006 topgele 21242 topontopn 21252 connima 21737 islocfin 21829 ptbasfi 21893 txdis 21944 neifil 22192 elfm3 22262 rnelfmlem 22264 alexsubALTlem3 22361 alexsubALTlem4 22362 utopsnneiplem 22559 lmclimf 23610 uniiccdif 23882 dv11cn 24301 plypf1 24505 2pthon3v 27449 hstoh 29790 dmdi2 29862 disjeq1f 30090 eulerpartlemd 31275 rrvdmss 31359 refssfne 33233 neibastop3 33237 topmeet 33239 topjoin 33240 fnemeet2 33242 fnejoin1 33243 bj-restuni 33904 heiborlem3 34539 funALTVeq 35384 disjeq 35418 lsatelbN 35593 lkrscss 35685 lshpset2N 35706 mapdrvallem2 38232 hdmaprnlem3eN 38445 hdmaplkr 38500 uneqsn 39742 ssrecnpr 40062 founiiun 40865 founiiun0 40881 caragendifcl 42233 |
Copyright terms: Public domain | W3C validator |