Theorem eqimss 3989

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

This proof depends on syntax axioms:   → wi 4   = wceq 1570   ⊆ wss 3899

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-9 2155  ax-ext 2733

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-cleq 2753  df-ss 3916

This theorem is used by:  eqimss2  3990  sspss  4050  uneqin  4235  difn0  4315  ssdisj  4413  uneqdifeq  4448  pweq  4571  pwpw0  4774  ssprsseq  4786  sssn  4787  snsspw  4804  unieq  4878  unissint  4932  pwpwssunieq  5064  elpwuni  5065  disjeq2  5074  disjeq1  5077  pwne  5314  pwssun  5543  poeq2  5563  freq2  5619  seeq1  5621  seeq2  5622  frsn  5739  dmxpss  6163  xp11  6167  dmsnopss  6214  trsucss  6452  suc11  6471  iotassuni  6512  funeq  6557  fnresdm  6656  fssxp  6735  ffdm  6737  fcoi1  6754  fof  6794  dff1o2  6828  fvmptss  7004  fvmptss2  7018  funressn  7161  dff1o6  7281  tposeq  8238  tfrlem11  8389  oewordi  8593  oewordri  8594  dffi3  9416  cantnfle  9665  cantnflem2  9684  r1ord3g  9779  rankeq0b  9869  rankxplim3  9891  carddom2  10051  cflm  10320  cfsuc  10328  isf32lem2  10425  axdc3lem2  10522  ttukeylem5  10584  tsksuc  10840  fsuppmapnn0fiublem  14126  fsuppmapnn0fiub  14127  xptrrel  15126  relexpnndm  15187  relexpdmg  15188  relexprng  15192  relexpfld  15195  relexpaddg  15199  invf  17936  sscres  17991  pgpssslw  19821  fislw  19832  frgpup1  19982  frgpup3lem  19984  dprdspan  20236  dprdz  20239  dprdf1o  20241  dprd2da  20251  ablfac1b  20279  lspsncmp  21387  lspsnne2  21389  lspsneq  21393  psgnghm2  21880  psrbaglesupp  22223  psrbaglefi  22227  mplcoe5  22342  mplbas2  22344  ofco2  22759  toprntopon  23236  cncnpi  23589  hauscmplem  23717  iskgen2  23860  elqtop3  24015  qtoprest  24029  hmeores  24083  snfil  24176  uffixfr  24235  ustuqtop2  24554  tngngp2  24964  metnrmlem3  25174  volcn  25920  recnprss  26217  plyeq0  26523  madebdaylemlrcut  28278  uhgr3cyclex  30776  chsupsn  32008  chlejb1i  32071  atsseq  32942  disjeq1f  33160  ldgenpisys  34792  measxun2  34836  measssd  34841  measiuns  34843  pmeasmono  34949  eulerpartlemb  34993  bnj1143  35413  bnj1322  35445  fnfvintima  35705  funsseq  36512  opnbnd  37093  cldbnd  37094  fnemeet1  37134  tz9.1tco  37251  bj-restuni  37998  bj-inexeqex  38055  bj-idreseq  38063  relowlpssretop  38267  pibt2  38320  ovoliunnfl  38560  voliunnfl  38562  volsupnfl  38563  heiborlem10  38734  smprngopr  38966  funALTVeq  39697  disjeq  39746  lshpcmp  40025  lsatcmp  40040  lsatcmp2  40041  lshpset2N  40156  paddasslem17  40873  pcl0bN  40960  pexmidALTN  41015  lcfrlem26  42605  lcfrlem36  42615  mapd0  42702  nacsfix  43702  minregex  44519  cbviuneq12df  44646  relexp0a  44701  relexpaddss  44703  frege124d  44746  k0004lem3  45134  dvconstbi  45303  ssin0  46041  icccncfext  46866  dvmptconst  46894  dvmptidg  46896  dvmulcncf  46904  dvdivcncf  46906  dirkercncflem2  47083  fourierdlem70  47155  fourierdlem71  47156  ovnsubaddlem1  47549  ovnhoi  47582  hspdifhsp  47595  fcoreslem4  48105  smprngprmrng  49405  iuneqconst2  49902  iineqconst2  49903  seppsepf  50006  intubeu  50061  setrec2mpt  50759  0setrec  50766