Theorem eqimss 3981

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 3979	1 ⊢ (𝐴 = 𝐵 → 𝐴 ⊆ 𝐵)

Syntax hints:   → wi 4   = wceq 1542   ⊆ wss 3890

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-9 2124  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1782  df-cleq 2729  df-ss 3907

This theorem is referenced by:  eqimss2  3982  sspss  4043  uneqin  4230  difn0  4308  ssdisj  4401  uneqdifeq  4433  pweq  4556  pwpw0  4757  ssprsseq  4769  sssn  4770  snsspw  4788  unieq  4862  unissint  4915  pwpwssunieq  5047  elpwuni  5048  disjeq2  5057  disjeq1  5060  pwne  5291  pwssun  5517  poeq2  5537  freq2  5593  seeq1  5595  seeq2  5596  frsn  5713  dmxpss  6130  xp11  6134  dmsnopss  6173  trsucss  6408  suc11  6427  iotassuni  6468  funeq  6513  fnresdm  6612  fssxp  6690  ffdm  6692  fcoi1  6709  fof  6747  dff1o2  6780  fvmptss  6955  fvmptss2  6969  funressn  7107  dff1o6  7224  tposeq  8172  tfrlem11  8321  oewordi  8521  oewordri  8522  dffi3  9338  cantnfle  9586  cantnflem2  9605  r1ord3g  9697  rankeq0b  9778  rankxplim3  9799  carddom2  9895  cflm  10166  cfsuc  10173  isf32lem2  10270  axdc3lem2  10367  ttukeylem5  10429  tsksuc  10679  fsuppmapnn0fiublem  13946  fsuppmapnn0fiub  13947  xptrrel  14936  relexpnndm  14997  relexpdmg  14998  relexprng  15002  relexpfld  15005  relexpaddg  15009  invf  17729  sscres  17784  pgpssslw  19583  fislw  19594  frgpup1  19744  frgpup3lem  19746  dprdspan  19998  dprdz  20001  dprdf1o  20003  dprd2da  20013  ablfac1b  20041  lspsncmp  21109  lspsnne2  21111  lspsneq  21115  psgnghm2  21574  psrbaglesupp  21915  psrbaglefi  21919  mplcoe5  22031  mplbas2  22033  ofco2  22429  toprntopon  22903  cncnpi  23256  hauscmplem  23384  iskgen2  23526  elqtop3  23681  qtoprest  23695  hmeores  23749  snfil  23842  uffixfr  23901  ustuqtop2  24220  tngngp2  24630  metnrmlem3  24840  volcn  25586  recnprss  25884  plyeq0  26189  madebdaylemlrcut  27908  uhgr3cyclex  30270  chsupsn  31502  chlejb1i  31565  atsseq  32436  disjeq1f  32661  ldgenpisys  34329  measxun2  34373  measssd  34378  measiuns  34380  pmeasmono  34487  eulerpartlemb  34531  bnj1143  34951  bnj1322  34983  funsseq  35969  opnbnd  36526  cldbnd  36527  fnemeet1  36567  tz9.1tco  36684  bj-restuni  37428  bj-inexeqex  37487  bj-idreseq  37495  relowlpssretop  37697  pibt2  37750  ovoliunnfl  38000  voliunnfl  38002  volsupnfl  38003  heiborlem10  38158  smprngopr  38390  funALTVeq  39123  disjeq  39172  lshpcmp  39451  lsatcmp  39466  lsatcmp2  39467  lshpset2N  39582  paddasslem17  40299  pcl0bN  40386  pexmidALTN  40441  lcfrlem26  42031  lcfrlem36  42041  mapd0  42128  nacsfix  43161  minregex  43982  cbviuneq12df  44109  relexp0a  44164  relexpaddss  44166  frege124d  44209  k0004lem3  44597  dvconstbi  44782  ssin0  45507  icccncfext  46336  dvmptconst  46364  dvmptidg  46366  dvmulcncf  46374  dvdivcncf  46376  dirkercncflem2  46553  fourierdlem70  46625  fourierdlem71  46626  ovnsubaddlem1  47019  ovnhoi  47052  hspdifhsp  47065  fcoreslem4  47529  iuneqconst2  49313  iineqconst2  49314  seppsepf  49419  intubeu  49474  setrec2mpt  50187  0setrec  50194