![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > eqimss2 | Structured version Visualization version GIF version |
Description: Equality implies inclusion. (Contributed by NM, 23-Nov-2003.) |
Ref | Expression |
---|---|
eqimss2 | ⊢ (𝐵 = 𝐴 → 𝐴 ⊆ 𝐵) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | eqimss 4035 | . 2 ⊢ (𝐴 = 𝐵 → 𝐴 ⊆ 𝐵) | |
2 | 1 | eqcoms 2733 | 1 ⊢ (𝐵 = 𝐴 → 𝐴 ⊆ 𝐵) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 = wceq 1533 ⊆ wss 3944 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1789 ax-4 1803 ax-5 1905 ax-6 1963 ax-7 2003 ax-9 2108 ax-ext 2696 |
This theorem depends on definitions: df-bi 206 df-an 395 df-ex 1774 df-cleq 2717 df-ss 3961 |
This theorem is referenced by: pweq 4618 ifpprsnss 4770 unieq 4920 disjeq2 5118 disjeq1 5121 poeq2 5594 freq2 5649 seeq1 5650 seeq2 5651 dmcoeq 5977 xp11 6181 suc11 6478 funeq 6574 fimadmfoALT 6821 foco 6824 fconst3 7225 sorpssuni 7738 sorpssint 7739 tposeq 8234 oaass 8582 odi 8600 oen0 8607 mapssfset 8870 inficl 9450 fodomfi2 10085 zorng 10529 rlimclim 15526 imasaddfnlem 17513 imasvscafn 17522 gasubg 19265 pgpssslw 19581 dprddisj2 20008 dprd2da 20011 imadrhmcl 20697 evlslem6 22049 topgele 22876 topontopn 22886 connima 23373 islocfin 23465 ptbasfi 23529 txdis 23580 neifil 23828 elfm3 23898 rnelfmlem 23900 alexsubALTlem3 23997 alexsubALTlem4 23998 utopsnneiplem 24196 lmclimf 25276 uniiccdif 25551 dv11cn 25978 plypf1 26191 2pthon3v 29826 hstoh 32114 dmdi2 32186 disjeq1f 32442 eulerpartlemd 34117 rrvdmss 34200 umgr2cycllem 34881 refssfne 35973 neibastop3 35977 topmeet 35979 topjoin 35980 fnemeet2 35982 fnejoin1 35983 bj-restuni 36707 bj-inexeqex 36764 bj-idreseq 36772 heiborlem3 37417 funALTVeq 38302 disjeq 38336 lsatelbN 38608 lkrscss 38700 lshpset2N 38721 mapdrvallem2 41248 hdmaprnlem3eN 41461 hdmaplkr 41516 uneqsn 43597 ssrecnpr 43887 founiiun 44691 founiiun0 44702 caragendifcl 46040 fnfocofob 46597 imasetpreimafvbijlemfo 46882 unilbeu 48182 |
Copyright terms: Public domain | W3C validator |