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  35745  opnbnd  36303  cldbnd  36304  fnemeet1  36344  bj-restuni  37075  bj-inexeqex  37132  bj-idreseq  37140  relowlpssretop  37342  pibt2  37395  ovoliunnfl  37646  voliunnfl  37648  volsupnfl  37649  heiborlem10  37804  smprngopr  38036  funALTVeq  38682  disjeq  38716  lshpcmp  38971  lsatcmp  38986  lsatcmp2  38987  lshpset2N  39102  paddasslem17  39819  pcl0bN  39906  pexmidALTN  39961  lcfrlem26  41551  lcfrlem36  41561  mapd0  41648  nacsfix  42689  minregex  43511  cbviuneq12df  43638  relexp0a  43693  relexpaddss  43695  frege124d  43738  k0004lem3  44126  dvconstbi  44311  ssin0  45037  icccncfext  45872  dvmptconst  45900  dvmptidg  45902  dvmulcncf  45910  dvdivcncf  45912  dirkercncflem2  46089  fourierdlem70  46161  fourierdlem71  46162  hoicvr  46533  ovnsubaddlem1  46555  ovnhoi  46588  hspdifhsp  46601  fcoreslem4  47054  iuneqconst2  48811  iineqconst2  48812  seppsepf  48917  intubeu  48972  setrec2mpt  49686  0setrec  49693