Theorem eqimss 3994

Description: Equality implies inclusion. (Contributed by NM, 21-Jun-1993.) (Proof shortened by Andrew Salmon, 21-Jun-2011.)

Assertion

Ref	Expression
eqimss	⊢ (𝐴 = 𝐵 → 𝐴 ⊆ 𝐵)

Proof of Theorem eqimss

Step	Hyp	Ref	Expression
1		id 22	. 2 ⊢ (𝐴 = 𝐵 → 𝐴 = 𝐵)
2	1	eqimssd 3992	1 ⊢ (𝐴 = 𝐵 → 𝐴 ⊆ 𝐵)

Syntax hints:   → wi 4   = wceq 1540   ⊆ wss 3903

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 2008  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-cleq 2721  df-ss 3920

This theorem is referenced by:  eqimss2  3995  sspss  4053  uneqin  4240  difn0  4318  ssdisj  4411  uneqdifeq  4444  pweq  4565  pwpw0  4764  ssprsseq  4776  sssn  4777  snsspw  4795  unieq  4869  unissint  4922  pwpwssunieq  5053  elpwuni  5054  disjeq2  5063  disjeq1  5066  pwne  5292  pwssun  5511  poeq2  5531  freq2  5587  seeq1  5589  seeq2  5590  frsn  5707  dmxpss  6120  xp11  6124  dmsnopss  6163  trsucss  6397  suc11  6416  iotassuni  6457  funeq  6502  fnresdm  6601  fssxp  6679  ffdm  6681  fcoi1  6698  fof  6736  dff1o2  6769  fvmptss  6942  fvmptss2  6956  funressn  7093  dff1o6  7212  tposeq  8161  tfrlem11  8310  oewordi  8509  oewordri  8510  dffi3  9321  cantnfle  9567  cantnflem2  9586  r1ord3g  9675  rankeq0b  9756  rankxplim3  9777  carddom2  9873  cflm  10144  cfsuc  10151  isf32lem2  10248  axdc3lem2  10345  ttukeylem5  10407  tsksuc  10656  fsuppmapnn0fiublem  13897  fsuppmapnn0fiub  13898  xptrrel  14887  relexpnndm  14948  relexpdmg  14949  relexprng  14953  relexpfld  14956  relexpaddg  14960  invf  17675  sscres  17730  pgpssslw  19493  fislw  19504  frgpup1  19654  frgpup3lem  19656  dprdspan  19908  dprdz  19911  dprdf1o  19913  dprd2da  19923  ablfac1b  19951  lspsncmp  21023  lspsnne2  21025  lspsneq  21029  psgnghm2  21488  psrbaglesupp  21829  psrbaglefi  21833  mplcoe5  21945  mplbas2  21947  ofco2  22336  toprntopon  22810  cncnpi  23163  hauscmplem  23291  iskgen2  23433  elqtop3  23588  qtoprest  23602  hmeores  23656  snfil  23749  uffixfr  23808  ustuqtop2  24128  tngngp2  24538  metnrmlem3  24748  volcn  25505  recnprss  25803  plyeq0  26114  madebdaylemlrcut  27813  uhgr3cyclex  30126  chsupsn  31357  chlejb1i  31420  atsseq  32291  disjeq1f  32517  ldgenpisys  34133  measxun2  34177  measssd  34182  measiuns  34184  pmeasmono  34292  eulerpartlemb  34336  bnj1143  34757  bnj1322  34789  funsseq  35741  opnbnd  36299  cldbnd  36300  fnemeet1  36340  bj-restuni  37071  bj-inexeqex  37128  bj-idreseq  37136  relowlpssretop  37338  pibt2  37391  ovoliunnfl  37642  voliunnfl  37644  volsupnfl  37645  heiborlem10  37800  smprngopr  38032  funALTVeq  38678  disjeq  38712  lshpcmp  38967  lsatcmp  38982  lsatcmp2  38983  lshpset2N  39098  paddasslem17  39815  pcl0bN  39902  pexmidALTN  39957  lcfrlem26  41547  lcfrlem36  41557  mapd0  41644  nacsfix  42685  minregex  43507  cbviuneq12df  43634  relexp0a  43689  relexpaddss  43691  frege124d  43734  k0004lem3  44122  dvconstbi  44307  ssin0  45033  icccncfext  45868  dvmptconst  45896  dvmptidg  45898  dvmulcncf  45906  dvdivcncf  45908  dirkercncflem2  46085  fourierdlem70  46157  fourierdlem71  46158  hoicvr  46529  ovnsubaddlem1  46551  ovnhoi  46584  hspdifhsp  46597  fcoreslem4  47050  iuneqconst2  48807  iineqconst2  48808  seppsepf  48913  intubeu  48968  setrec2mpt  49682  0setrec  49689