![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > eqimss | Structured version Visualization version GIF version |
Description: Equality implies the subclass relation. (Contributed by NM, 21-Jun-1993.) (Proof shortened by Andrew Salmon, 21-Jun-2011.) |
Ref | Expression |
---|---|
eqimss | ⊢ (𝐴 = 𝐵 → 𝐴 ⊆ 𝐵) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | eqss 3869 | . 2 ⊢ (𝐴 = 𝐵 ↔ (𝐴 ⊆ 𝐵 ∧ 𝐵 ⊆ 𝐴)) | |
2 | 1 | simplbi 490 | 1 ⊢ (𝐴 = 𝐵 → 𝐴 ⊆ 𝐵) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 = wceq 1507 ⊆ wss 3825 |
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 1964 ax-8 2050 ax-9 2057 ax-10 2077 ax-11 2091 ax-12 2104 ax-ext 2745 |
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 2014 df-clab 2754 df-cleq 2765 df-clel 2840 df-in 3832 df-ss 3839 |
This theorem is referenced by: eqimss2 3910 sspss 3962 uneqin 4137 difn0 4205 ssdisj 4286 uneqdifeq 4315 pwpw0 4614 ssprsseq 4626 sssn 4627 snsspw 4643 pwsnALT 4699 unissint 4767 pwpwssunieq 4886 elpwuni 4887 disjeq2 4895 disjeq1 4898 pwne 5101 pwssun 5301 poeq2 5323 freq2 5371 seeq1 5372 seeq2 5373 frsn 5482 dmxpss 5862 xp11 5866 dmsnopss 5904 trsucss 6108 suc11 6126 iotassuni 6162 funeq 6202 fnresdm 6293 fssxp 6357 ffdm 6359 fcoi1 6375 fof 6413 dff1o2 6443 fvmptss 6600 fvmptss2 6613 funressn 6738 dff1o6 6851 suceloni 7338 tposeq 7690 tfrlem11 7821 oewordi 8010 oewordri 8011 dffi3 8682 cantnfle 8920 cantnflem2 8939 r1ord3g 8994 rankeq0b 9075 rankxplim3 9096 carddom2 9192 cflm 9462 cfsuc 9469 isf32lem2 9566 axdc3lem2 9663 ttukeylem5 9725 tsksuc 9974 fsuppmapnn0fiublem 13166 fsuppmapnn0fiub 13167 xptrrel 14191 relexpnndm 14251 relexpdmg 14252 relexprng 14256 relexpfld 14259 relexpaddg 14263 invf 16886 sscres 16941 pgpssslw 18490 fislw 18501 frgpup1 18651 frgpup3lem 18653 dprdspan 18889 dprdz 18892 dprdf1o 18894 dprd2da 18904 ablfac1b 18932 lspsncmp 19600 lspsnne2 19602 lspsneq 19606 psrbaglesupp 19852 psrbaglefi 19856 mplcoe5 19952 mplbas2 19954 psgnghm2 20417 ofco2 20754 toprntopon 21227 cncnpi 21580 hauscmplem 21708 iskgen2 21850 elqtop3 22005 qtoprest 22019 hmeores 22073 snfil 22166 uffixfr 22225 ustuqtop2 22544 tngngp2 22954 metnrmlem3 23162 volcn 23900 recnprss 24195 plyeq0 24494 uhgr3cyclex 27701 chsupsn 28961 chlejb1i 29024 atsseq 29895 disjeq1f 30080 ldgenpisys 31027 measxun2 31071 measssd 31076 measiuns 31078 pmeasmono 31184 eulerpartlemb 31228 bnj1143 31671 bnj1322 31703 funsseq 32471 opnbnd 33134 cldbnd 33135 fnemeet1 33175 bj-restuni 33833 relowlpssretop 34022 pibt2 34074 ovoliunnfl 34323 voliunnfl 34325 volsupnfl 34326 heiborlem10 34488 smprngopr 34720 funALTVeq 35326 disjeq 35360 lshpcmp 35517 lsatcmp 35532 lsatcmp2 35533 lshpset2N 35648 paddasslem17 36365 pcl0bN 36452 pexmidALTN 36507 lcfrlem26 38097 lcfrlem36 38107 mapd0 38194 nacsfix 38649 cbviuneq12df 39314 relexp0a 39369 relexpaddss 39371 frege124d 39414 k0004lem3 39807 dvconstbi 40026 ssin0 40681 icccncfext 41546 dvmptconst 41575 dvmptidg 41577 dvmulcncf 41586 dvdivcncf 41588 dirkercncflem2 41766 fourierdlem70 41838 fourierdlem71 41839 hoicvr 42207 ovnsubaddlem1 42229 ovnhoi 42262 hspdifhsp 42275 0setrec 44113 |
Copyright terms: Public domain | W3C validator |