Theorem eqimss 4003

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 23	. 2 ⊢ (𝐴 = 𝐵 → 𝐴 = 𝐵)
2	1	eqimssd 4001	1 ⊢ (𝐴 = 𝐵 → 𝐴 ⊆ 𝐵)

Syntax hints:   → wi 4   = wceq 1567   ⊆ wss 3913

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937  ax-6 1994  ax-7 2035  ax-9 2159  ax-ext 2741

This theorem depends on definitions:  df-bi 210  df-an 401  df-ex 1807  df-cleq 2761  df-ss 3930

This theorem is referenced by:  eqimss2  4004  sspss  4064  uneqin  4250  difn0  4330  ssdisj  4426  uneqdifeq  4458  pweq  4581  pwpw0  4783  ssprsseq  4795  sssn  4796  snsspw  4813  unieq  4887  unissint  4941  pwpwssunieq  5074  elpwuni  5075  disjeq2  5084  disjeq1  5087  pwne  5324  pwssun  5554  poeq2  5574  freq2  5630  seeq1  5632  seeq2  5633  frsn  5750  dmxpss  6170  xp11  6174  dmsnopss  6216  trsucss  6452  suc11  6471  iotassuni  6512  funeq  6557  fnresdm  6655  fssxp  6734  ffdm  6736  fcoi1  6753  fof  6793  dff1o2  6827  fvmptss  7003  fvmptss2  7017  funressn  7157  dff1o6  7274  tposeq  8224  tfrlem11  8375  oewordi  8577  oewordri  8578  dffi3  9391  cantnfle  9640  cantnflem2  9659  r1ord3g  9751  rankeq0b  9832  rankxplim3  9853  carddom2  9963  cflm  10233  cfsuc  10241  isf32lem2  10338  axdc3lem2  10435  ttukeylem5  10497  tsksuc  10747  fsuppmapnn0fiublem  14026  fsuppmapnn0fiub  14027  xptrrel  15017  relexpnndm  15078  relexpdmg  15079  relexprng  15083  relexpfld  15086  relexpaddg  15090  invf  17825  sscres  17880  pgpssslw  19684  fislw  19695  frgpup1  19845  frgpup3lem  19847  dprdspan  20099  dprdz  20102  dprdf1o  20104  dprd2da  20114  ablfac1b  20142  lspsncmp  21218  lspsnne2  21220  lspsneq  21224  psgnghm2  21700  psrbaglesupp  22041  psrbaglefi  22045  mplcoe5  22160  mplbas2  22162  ofco2  22577  toprntopon  23051  cncnpi  23404  hauscmplem  23532  iskgen2  23674  elqtop3  23829  qtoprest  23843  hmeores  23897  snfil  23990  uffixfr  24049  ustuqtop2  24368  tngngp2  24778  metnrmlem3  24988  volcn  25734  recnprss  26032  plyeq0  26337  madebdaylemlrcut  28058  uhgr3cyclex  30474  chsupsn  31706  chlejb1i  31769  atsseq  32640  disjeq1f  32859  ldgenpisys  34501  measxun2  34545  measssd  34550  measiuns  34552  pmeasmono  34659  eulerpartlemb  34703  bnj1143  35123  bnj1322  35155  funsseq  36193  opnbnd  36759  cldbnd  36760  fnemeet1  36800  tz9.1tco  36917  bj-restuni  37661  bj-inexeqex  37720  bj-idreseq  37728  relowlpssretop  37932  pibt2  37985  ovoliunnfl  38235  voliunnfl  38237  volsupnfl  38238  heiborlem10  38393  smprngopr  38625  funALTVeq  39358  disjeq  39407  lshpcmp  39686  lsatcmp  39701  lsatcmp2  39702  lshpset2N  39817  paddasslem17  40534  pcl0bN  40621  pexmidALTN  40676  lcfrlem26  42266  lcfrlem36  42276  mapd0  42363  nacsfix  43369  minregex  44186  cbviuneq12df  44313  relexp0a  44368  relexpaddss  44370  frege124d  44413  k0004lem3  44801  dvconstbi  44970  ssin0  45701  icccncfext  46527  dvmptconst  46555  dvmptidg  46557  dvmulcncf  46565  dvdivcncf  46567  dirkercncflem2  46744  fourierdlem70  46816  fourierdlem71  46817  ovnsubaddlem1  47210  ovnhoi  47243  hspdifhsp  47256  fcoreslem4  47726  smprngprmrng  49027  iuneqconst2  49520  iineqconst2  49521  seppsepf  49626  intubeu  49681  setrec2mpt  50394  0setrec  50401