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  8223  tfrlem11  8374  oewordi  8576  oewordri  8577  dffi3  9390  cantnfle  9639  cantnflem2  9658  r1ord3g  9750  rankeq0b  9831  rankxplim3  9852  carddom2  9962  cflm  10232  cfsuc  10240  isf32lem2  10337  axdc3lem2  10434  ttukeylem5  10496  tsksuc  10746  fsuppmapnn0fiublem  14025  fsuppmapnn0fiub  14026  xptrrel  15016  relexpnndm  15077  relexpdmg  15078  relexprng  15082  relexpfld  15085  relexpaddg  15089  invf  17824  sscres  17879  pgpssslw  19683  fislw  19694  frgpup1  19844  frgpup3lem  19846  dprdspan  20098  dprdz  20101  dprdf1o  20103  dprd2da  20113  ablfac1b  20141  lspsncmp  21217  lspsnne2  21219  lspsneq  21223  psgnghm2  21699  psrbaglesupp  22040  psrbaglefi  22044  mplcoe5  22159  mplbas2  22161  ofco2  22576  toprntopon  23050  cncnpi  23403  hauscmplem  23531  iskgen2  23673  elqtop3  23828  qtoprest  23842  hmeores  23896  snfil  23989  uffixfr  24048  ustuqtop2  24367  tngngp2  24777  metnrmlem3  24987  volcn  25733  recnprss  26031  plyeq0  26336  madebdaylemlrcut  28057  uhgr3cyclex  30473  chsupsn  31705  chlejb1i  31768  atsseq  32639  disjeq1f  32858  ldgenpisys  34500  measxun2  34544  measssd  34549  measiuns  34551  pmeasmono  34658  eulerpartlemb  34702  bnj1143  35122  bnj1322  35154  funsseq  36158  opnbnd  36724  cldbnd  36725  fnemeet1  36765  tz9.1tco  36882  bj-restuni  37626  bj-inexeqex  37685  bj-idreseq  37693  relowlpssretop  37897  pibt2  37950  ovoliunnfl  38200  voliunnfl  38202  volsupnfl  38203  heiborlem10  38358  smprngopr  38590  funALTVeq  39323  disjeq  39372  lshpcmp  39651  lsatcmp  39666  lsatcmp2  39667  lshpset2N  39782  paddasslem17  40499  pcl0bN  40586  pexmidALTN  40641  lcfrlem26  42231  lcfrlem36  42241  mapd0  42328  nacsfix  43334  minregex  44151  cbviuneq12df  44278  relexp0a  44333  relexpaddss  44335  frege124d  44378  k0004lem3  44766  dvconstbi  44935  ssin0  45666  icccncfext  46492  dvmptconst  46520  dvmptidg  46522  dvmulcncf  46530  dvdivcncf  46532  dirkercncflem2  46709  fourierdlem70  46781  fourierdlem71  46782  ovnsubaddlem1  47175  ovnhoi  47208  hspdifhsp  47221  fcoreslem4  47691  smprngprmrng  48992  iuneqconst2  49485  iineqconst2  49486  seppsepf  49591  intubeu  49646  setrec2mpt  50359  0setrec  50366