Theorem eqimss 4005

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

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

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 3931

This theorem is referenced by:  eqimss2  4006  sspss  4065  uneqin  4252  difn0  4330  ssdisj  4423  uneqdifeq  4456  pweq  4577  pwpw0  4777  ssprsseq  4789  sssn  4790  snsspw  4808  unieq  4882  unissint  4936  pwpwssunieq  5068  elpwuni  5069  disjeq2  5078  disjeq1  5081  pwne  5308  pwssun  5530  poeq2  5550  freq2  5606  seeq1  5608  seeq2  5609  frsn  5726  dmxpss  6144  xp11  6148  dmsnopss  6187  trsucss  6422  suc11  6441  iotassuni  6483  iotassuniOLD  6490  funeq  6536  fnresdm  6637  fssxp  6715  ffdm  6717  fcoi1  6734  fof  6772  dff1o2  6805  fvmptss  6980  fvmptss2  6994  funressn  7131  dff1o6  7250  sucexeloniOLD  7786  tposeq  8207  tfrlem11  8356  oewordi  8555  oewordri  8556  dffi3  9382  cantnfle  9624  cantnflem2  9643  r1ord3g  9732  rankeq0b  9813  rankxplim3  9834  carddom2  9930  cflm  10203  cfsuc  10210  isf32lem2  10307  axdc3lem2  10404  ttukeylem5  10466  tsksuc  10715  fsuppmapnn0fiublem  13955  fsuppmapnn0fiub  13956  xptrrel  14946  relexpnndm  15007  relexpdmg  15008  relexprng  15012  relexpfld  15015  relexpaddg  15019  invf  17730  sscres  17785  pgpssslw  19544  fislw  19555  frgpup1  19705  frgpup3lem  19707  dprdspan  19959  dprdz  19962  dprdf1o  19964  dprd2da  19974  ablfac1b  20002  lspsncmp  21026  lspsnne2  21028  lspsneq  21032  psgnghm2  21490  psrbaglesupp  21831  psrbaglefi  21835  mplcoe5  21947  mplbas2  21949  ofco2  22338  toprntopon  22812  cncnpi  23165  hauscmplem  23293  iskgen2  23435  elqtop3  23590  qtoprest  23604  hmeores  23658  snfil  23751  uffixfr  23810  ustuqtop2  24130  tngngp2  24540  metnrmlem3  24750  volcn  25507  recnprss  25805  plyeq0  26116  madebdaylemlrcut  27810  uhgr3cyclex  30111  chsupsn  31342  chlejb1i  31405  atsseq  32276  disjeq1f  32502  ldgenpisys  34156  measxun2  34200  measssd  34205  measiuns  34207  pmeasmono  34315  eulerpartlemb  34359  bnj1143  34780  bnj1322  34812  funsseq  35755  opnbnd  36313  cldbnd  36314  fnemeet1  36354  bj-restuni  37085  bj-inexeqex  37142  bj-idreseq  37150  relowlpssretop  37352  pibt2  37405  ovoliunnfl  37656  voliunnfl  37658  volsupnfl  37659  heiborlem10  37814  smprngopr  38046  funALTVeq  38692  disjeq  38726  lshpcmp  38981  lsatcmp  38996  lsatcmp2  38997  lshpset2N  39112  paddasslem17  39830  pcl0bN  39917  pexmidALTN  39972  lcfrlem26  41562  lcfrlem36  41572  mapd0  41659  nacsfix  42700  minregex  43523  cbviuneq12df  43650  relexp0a  43705  relexpaddss  43707  frege124d  43750  k0004lem3  44138  dvconstbi  44323  ssin0  45049  icccncfext  45885  dvmptconst  45913  dvmptidg  45915  dvmulcncf  45923  dvdivcncf  45925  dirkercncflem2  46102  fourierdlem70  46174  fourierdlem71  46175  hoicvr  46546  ovnsubaddlem1  46568  ovnhoi  46601  hspdifhsp  46614  fcoreslem4  47067  iuneqconst2  48811  iineqconst2  48812  seppsepf  48917  intubeu  48972  setrec2mpt  49686  0setrec  49693