| 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 4042 | . 2 ⊢ (𝐴 = 𝐵 → 𝐴 ⊆ 𝐵) | |
| 2 | 1 | eqcoms 2745 | 1 ⊢ (𝐵 = 𝐴 → 𝐴 ⊆ 𝐵) |
| Colors of variables: wff setvar class |
| Syntax hints: → wi 4 = wceq 1540 ⊆ wss 3951 |
| This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1795 ax-4 1809 ax-5 1910 ax-6 1967 ax-7 2007 ax-9 2118 ax-ext 2708 |
| This theorem depends on definitions: df-bi 207 df-an 396 df-ex 1780 df-cleq 2729 df-ss 3968 |
| This theorem is referenced by: pweq 4614 ifpprsnss 4764 unieq 4918 disjeq2 5114 disjeq1 5117 poeq2 5596 freq2 5653 seeq1 5655 seeq2 5656 dmcoeq 5989 xp11 6195 suc11 6491 funeq 6586 fimadmfoALT 6831 foco 6834 fconst3 7233 sorpssuni 7752 sorpssint 7753 tposeq 8253 oaass 8599 odi 8617 oen0 8624 mapssfset 8891 inficl 9465 fodomfi2 10100 zorng 10544 rlimclim 15582 imasaddfnlem 17573 imasvscafn 17582 gasubg 19320 pgpssslw 19632 dprddisj2 20059 dprd2da 20062 imadrhmcl 20798 evlslem6 22105 topgele 22936 topontopn 22946 connima 23433 islocfin 23525 ptbasfi 23589 txdis 23640 neifil 23888 elfm3 23958 rnelfmlem 23960 alexsubALTlem3 24057 alexsubALTlem4 24058 utopsnneiplem 24256 lmclimf 25338 uniiccdif 25613 dv11cn 26040 plypf1 26251 2pthon3v 29963 hstoh 32251 dmdi2 32323 disjeq1f 32586 eulerpartlemd 34368 rrvdmss 34451 umgr2cycllem 35145 refssfne 36359 neibastop3 36363 topmeet 36365 topjoin 36366 fnemeet2 36368 fnejoin1 36369 bj-restuni 37098 bj-inexeqex 37155 bj-idreseq 37163 heiborlem3 37820 funALTVeq 38701 disjeq 38735 lsatelbN 39007 lkrscss 39099 lshpset2N 39120 mapdrvallem2 41647 hdmaprnlem3eN 41860 hdmaplkr 41915 uneqsn 44038 ssrecnpr 44327 founiiun 45184 founiiun0 45195 caragendifcl 46529 fnfocofob 47091 imasetpreimafvbijlemfo 47392 unilbeu 48874 |
| Copyright terms: Public domain | W3C validator |