Theorem eqimss 3995

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

Syntax hints:   → wi 4   = wceq 1570   ⊆ wss 3905

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-9 2153  ax-ext 2735

This theorem depends on definitions:  df-bi 210  df-an 401  df-ex 1810  df-cleq 2755  df-ss 3922

This theorem is referenced by:  eqimss2  3996  sspss  4056  uneqin  4242  difn0  4322  ssdisj  4420  uneqdifeq  4453  pweq  4576  pwpw0  4779  ssprsseq  4791  sssn  4792  snsspw  4809  unieq  4883  unissint  4937  pwpwssunieq  5070  elpwuni  5071  disjeq2  5080  disjeq1  5083  pwne  5323  pwssun  5553  poeq2  5573  freq2  5629  seeq1  5631  seeq2  5632  frsn  5749  dmxpss  6169  xp11  6173  dmsnopss  6215  trsucss  6451  suc11  6470  iotassuni  6511  funeq  6556  fnresdm  6654  fssxp  6733  ffdm  6735  fcoi1  6752  fof  6792  dff1o2  6826  fvmptss  7002  fvmptss2  7016  funressn  7156  dff1o6  7273  tposeq  8220  tfrlem11  8371  oewordi  8573  oewordri  8574  dffi3  9387  cantnfle  9636  cantnflem2  9655  r1ord3g  9747  rankeq0b  9828  rankxplim3  9849  carddom2  9959  cflm  10228  cfsuc  10236  isf32lem2  10333  axdc3lem2  10430  ttukeylem5  10492  tsksuc  10742  fsuppmapnn0fiublem  14022  fsuppmapnn0fiub  14023  xptrrel  15013  relexpnndm  15074  relexpdmg  15075  relexprng  15079  relexpfld  15082  relexpaddg  15086  invf  17820  sscres  17875  pgpssslw  19679  fislw  19690  frgpup1  19840  frgpup3lem  19842  dprdspan  20094  dprdz  20097  dprdf1o  20099  dprd2da  20109  ablfac1b  20137  lspsncmp  21240  lspsnne2  21242  lspsneq  21246  psgnghm2  21731  psrbaglesupp  22072  psrbaglefi  22076  mplcoe5  22191  mplbas2  22193  ofco2  22608  toprntopon  23082  cncnpi  23435  hauscmplem  23563  iskgen2  23705  elqtop3  23860  qtoprest  23874  hmeores  23928  snfil  24021  uffixfr  24080  ustuqtop2  24399  tngngp2  24809  metnrmlem3  25019  volcn  25765  recnprss  26063  plyeq0  26368  madebdaylemlrcut  28092  uhgr3cyclex  30533  chsupsn  31765  chlejb1i  31828  atsseq  32699  disjeq1f  32918  ldgenpisys  34556  measxun2  34600  measssd  34605  measiuns  34607  pmeasmono  34714  eulerpartlemb  34758  bnj1143  35178  bnj1322  35210  fnfvintima  35476  funsseq  36260  opnbnd  36836  cldbnd  36837  fnemeet1  36877  tz9.1tco  36994  bj-restuni  37739  bj-inexeqex  37798  bj-idreseq  37806  relowlpssretop  38010  pibt2  38063  ovoliunnfl  38313  voliunnfl  38315  volsupnfl  38316  heiborlem10  38471  smprngopr  38703  funALTVeq  39434  disjeq  39483  lshpcmp  39762  lsatcmp  39777  lsatcmp2  39778  lshpset2N  39893  paddasslem17  40610  pcl0bN  40697  pexmidALTN  40752  lcfrlem26  42342  lcfrlem36  42352  mapd0  42439  nacsfix  43443  minregex  44260  cbviuneq12df  44387  relexp0a  44442  relexpaddss  44444  frege124d  44487  k0004lem3  44875  dvconstbi  45044  ssin0  45775  icccncfext  46601  dvmptconst  46629  dvmptidg  46631  dvmulcncf  46639  dvdivcncf  46641  dirkercncflem2  46818  fourierdlem70  46890  fourierdlem71  46891  ovnsubaddlem1  47284  ovnhoi  47317  hspdifhsp  47330  fcoreslem4  47803  smprngprmrng  49104  iuneqconst2  49601  iineqconst2  49602  seppsepf  49707  intubeu  49762  setrec2mpt  50475  0setrec  50482