Theorem eqimss 3971

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

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

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 1945  ax-6 2002  ax-7 2043  ax-9 2157  ax-ext 2735

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

This theorem is used by:  eqimss2  3972  sspss  4032  uneqin  4237  difn0  4318  ssdisj  4416  uneqdifeq  4451  pweq  4574  ssprsseq  4786  sssn  4787  snsspw  4804  pwpw0  4836  unieq  4883  unissint  4937  pwpwssunieq  5069  elpwuni  5070  disjeq2  5079  disjeq1  5082  pwne  5321  pwssun  5550  poeq2  5570  freq2  5626  seeq1  5628  seeq2  5629  frsn  5747  dmxpss  6181  xp11  6185  dmsnopss  6234  trsucss  6479  suc11  6498  iotassuni  6540  funeq  6587  fnresdm  6688  fssxp  6767  ffdm  6769  fcoi1  6786  fof  6826  dff1o2  6860  fvmptss  7037  fvmptss2  7051  funressn  7195  dff1o6  7314  tposeq  8283  tfrlem11  8434  oewordi  8638  oewordri  8639  dffi3  9460  cantnfle  9709  cantnflem2  9728  r1ord3g  9823  rankeq0b  9913  rankxplim3  9935  carddom2  10095  cflm  10366  cfsuc  10374  isf32lem2  10471  axdc3lem2  10568  ttukeylem5  10630  tsksuc  10886  fsuppmapnn0fiublem  14173  fsuppmapnn0fiub  14174  xptrrel  15176  relexpnndm  15237  relexpdmg  15238  relexprng  15242  relexpfld  15245  relexpaddg  15249  invf  17993  sscres  18048  pgpssslw  19879  fislw  19890  frgpup1  20040  frgpup3lem  20042  dprdspan  20294  dprdz  20297  dprdf1o  20299  dprd2da  20309  ablfac1b  20337  lspsncmp  21445  lspsnne2  21447  lspsneq  21451  psgnghm2  21942  psrbaglesupp  22285  psrbaglefi  22289  mplcoe5  22404  mplbas2  22406  ofco2  22821  toprntopon  23298  cncnpi  23651  hauscmplem  23779  iskgen2  23922  elqtop3  24077  qtoprest  24091  hmeores  24145  snfil  24238  uffixfr  24297  ustuqtop2  24616  tngngp2  25026  metnrmlem3  25236  volcn  25982  recnprss  26279  plyeq0  26585  madebdaylemlrcut  28342  uhgr3cyclex  30840  chsupsn  32072  chlejb1i  32135  atsseq  33006  disjeq1f  33265  ldgenpisys  34910  measxun2  34954  measssd  34959  measiuns  34961  pmeasmono  35067  eulerpartlemb  35111  bnj1143  35531  bnj1322  35563  fnfvintima  35827  funsseq  36748  opnbnd  37328  cldbnd  37329  fnemeet1  37369  tz9.1tco  37486  bj-restuni  38288  bj-inexeqex  38343  bj-idreseq  38351  relowlpssretop  38555  pibt2  38608  ovoliunnfl  38848  voliunnfl  38850  volsupnfl  38851  heiborlem10  39020  smprngopr  39252  funALTVeq  39983  disjeq  40032  lshpcmp  40311  lsatcmp  40326  lsatcmp2  40327  lshpset2N  40442  paddasslem17  41159  pcl0bN  41246  pexmidALTN  41301  lcfrlem26  42891  lcfrlem36  42901  mapd0  42988  nacsfix  43989  minregex  44796  cbviuneq12df  44922  relexp0a  44977  relexpaddss  44979  frege124d  45022  k0004lem3  45410  dvconstbi  45579  ssin0  46346  icccncfext  47170  dvmptconst  47198  dvmptidg  47200  dvmulcncf  47208  dvdivcncf  47210  dirkercncflem2  47387  fourierdlem70  47459  fourierdlem71  47460  ovnsubaddlem1  47853  ovnhoi  47886  hspdifhsp  47899  fcoreslem4  48409  smprngprmrng  49767  iuneqconst2  50265  iineqconst2  50266  seppsepf  50374  intubeu  50429  setrec2mpt  51196  0setrec  51203