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 4020 | . 2 ⊢ (𝐴 = 𝐵 → 𝐴 ⊆ 𝐵) | |
2 | 1 | eqcoms 2826 | 1 ⊢ (𝐵 = 𝐴 → 𝐴 ⊆ 𝐵) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 = wceq 1528 ⊆ wss 3933 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1787 ax-4 1801 ax-5 1902 ax-6 1961 ax-7 2006 ax-8 2107 ax-9 2115 ax-10 2136 ax-11 2151 ax-12 2167 ax-ext 2790 |
This theorem depends on definitions: df-bi 208 df-an 397 df-or 842 df-tru 1531 df-ex 1772 df-nf 1776 df-sb 2061 df-clab 2797 df-cleq 2811 df-clel 2890 df-in 3940 df-ss 3949 |
This theorem is referenced by: ifpprsnss 4692 disjeq2 5026 disjeq1 5029 poeq2 5471 freq2 5519 seeq1 5520 seeq2 5521 dmcoeq 5838 xp11 6025 suc11 6287 funeq 6368 fimadmfoALT 6594 fconst3 6967 sorpssuni 7447 sorpssint 7448 tposeq 7883 oaass 8176 odi 8194 oen0 8201 inficl 8877 fodomfi2 9474 zorng 9914 rlimclim 14891 imasaddfnlem 16789 imasvscafn 16798 gasubg 18370 pgpssslw 18668 dprddisj2 19090 dprd2da 19093 evlslem6 20222 topgele 21466 topontopn 21476 connima 21961 islocfin 22053 ptbasfi 22117 txdis 22168 neifil 22416 elfm3 22486 rnelfmlem 22488 alexsubALTlem3 22585 alexsubALTlem4 22586 utopsnneiplem 22783 lmclimf 23834 uniiccdif 24106 dv11cn 24525 plypf1 24729 2pthon3v 27649 hstoh 29936 dmdi2 30008 disjeq1f 30251 eulerpartlemd 31523 rrvdmss 31606 umgr2cycllem 32284 refssfne 33603 neibastop3 33607 topmeet 33609 topjoin 33610 fnemeet2 33612 fnejoin1 33613 bj-restuni 34282 bj-inexeqex 34338 bj-idreseq 34346 heiborlem3 34972 funALTVeq 35813 disjeq 35847 lsatelbN 36022 lkrscss 36114 lshpset2N 36135 mapdrvallem2 38661 hdmaprnlem3eN 38874 hdmaplkr 38929 uneqsn 40251 ssrecnpr 40517 founiiun 41311 founiiun0 41327 caragendifcl 42673 imasetpreimafvbijlemfo 43442 |
Copyright terms: Public domain | W3C validator |