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 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-cleq 2752  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  5317  pwssun  5547  poeq2  5567  freq2  5623  seeq1  5625  seeq2  5626  frsn  5743  dmxpss  6164  xp11  6168  dmsnopss  6210  trsucss  6448  suc11  6467  iotassuni  6508  funeq  6553  fnresdm  6651  fssxp  6730  ffdm  6732  fcoi1  6749  fof  6789  dff1o2  6823  fvmptss  6999  fvmptss2  7013  funressn  7156  dff1o6  7276  tposeq  8226  tfrlem11  8377  oewordi  8579  oewordri  8580  dffi3  9401  cantnfle  9650  cantnflem2  9669  r1ord3g  9761  rankeq0b  9842  rankxplim3  9863  carddom2  9982  cflm  10251  cfsuc  10259  isf32lem2  10356  axdc3lem2  10453  ttukeylem5  10515  tsksuc  10771  fsuppmapnn0fiublem  14054  fsuppmapnn0fiub  14055  xptrrel  15053  relexpnndm  15114  relexpdmg  15115  relexprng  15119  relexpfld  15122  relexpaddg  15126  invf  17857  sscres  17912  pgpssslw  19741  fislw  19752  frgpup1  19902  frgpup3lem  19904  dprdspan  20156  dprdz  20159  dprdf1o  20161  dprd2da  20171  ablfac1b  20199  lspsncmp  21303  lspsnne2  21305  lspsneq  21309  psgnghm2  21794  psrbaglesupp  22137  psrbaglefi  22141  mplcoe5  22256  mplbas2  22258  ofco2  22673  toprntopon  23150  cncnpi  23503  hauscmplem  23631  iskgen2  23774  elqtop3  23929  qtoprest  23943  hmeores  23997  snfil  24090  uffixfr  24149  ustuqtop2  24468  tngngp2  24878  metnrmlem3  25088  volcn  25834  recnprss  26131  plyeq0  26437  madebdaylemlrcut  28164  uhgr3cyclex  30662  chsupsn  31894  chlejb1i  31957  atsseq  32828  disjeq1f  33046  ldgenpisys  34677  measxun2  34721  measssd  34726  measiuns  34728  pmeasmono  34835  eulerpartlemb  34879  bnj1143  35299  bnj1322  35331  fnfvintima  35591  funsseq  36347  opnbnd  36944  cldbnd  36945  fnemeet1  36985  tz9.1tco  37102  bj-restuni  37847  bj-inexeqex  37906  bj-idreseq  37914  relowlpssretop  38118  pibt2  38171  ovoliunnfl  38411  voliunnfl  38413  volsupnfl  38414  heiborlem10  38570  smprngopr  38802  funALTVeq  39533  disjeq  39582  lshpcmp  39861  lsatcmp  39876  lsatcmp2  39877  lshpset2N  39992  paddasslem17  40709  pcl0bN  40796  pexmidALTN  40851  lcfrlem26  42441  lcfrlem36  42451  mapd0  42538  nacsfix  43557  minregex  44374  cbviuneq12df  44501  relexp0a  44556  relexpaddss  44558  frege124d  44601  k0004lem3  44989  dvconstbi  45158  ssin0  45889  icccncfext  46715  dvmptconst  46743  dvmptidg  46745  dvmulcncf  46753  dvdivcncf  46755  dirkercncflem2  46932  fourierdlem70  47004  fourierdlem71  47005  ovnsubaddlem1  47398  ovnhoi  47431  hspdifhsp  47444  fcoreslem4  47954  smprngprmrng  49254  iuneqconst2  49751  iineqconst2  49752  seppsepf  49855  intubeu  49910  setrec2mpt  50623  0setrec  50630