Theorem eqimss 3978

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		eqss 3937	. 2 ⊢ (𝐴 = 𝐵 ↔ (𝐴 ⊆ 𝐵 ∧ 𝐵 ⊆ 𝐴))
2	1	simplbi 498	1 ⊢ (𝐴 = 𝐵 → 𝐴 ⊆ 𝐵)

Syntax hints:   → wi 4   = wceq 1539   ⊆ wss 3888

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2710

This theorem depends on definitions:  df-bi 206  df-an 397  df-tru 1542  df-ex 1783  df-sb 2069  df-clab 2717  df-cleq 2731  df-clel 2817  df-v 3435  df-in 3895  df-ss 3905

This theorem is referenced by:  eqimss2  3979  sspss  4035  uneqin  4213  difn0  4299  ssdisj  4394  uneqdifeq  4424  pweq  4550  pwpw0  4747  ssprsseq  4759  sssn  4760  snsspw  4776  pwsnOLD  4833  unieq  4851  unissint  4904  pwpwssunieq  5034  elpwuni  5035  disjeq2  5044  disjeq1  5047  pwne  5274  pwssun  5486  poeq2  5508  freq2  5561  seeq1  5562  seeq2  5563  frsn  5675  dmxpss  6079  xp11  6083  dmsnopss  6122  trsucss  6355  suc11  6373  iotassuni  6416  funeq  6461  fnresdm  6560  fssxp  6637  ffdm  6639  fcoi1  6657  fof  6697  dff1o2  6730  fvmptss  6896  fvmptss2  6909  funressn  7040  dff1o6  7156  sucexeloni  7667  suceloniOLD  7669  tposeq  8053  tfrlem11  8228  oewordi  8431  oewordri  8432  dffi3  9199  cantnfle  9438  cantnflem2  9457  r1ord3g  9546  rankeq0b  9627  rankxplim3  9648  carddom2  9744  cflm  10015  cfsuc  10022  isf32lem2  10119  axdc3lem2  10216  ttukeylem5  10278  tsksuc  10527  fsuppmapnn0fiublem  13719  fsuppmapnn0fiub  13720  xptrrel  14700  relexpnndm  14761  relexpdmg  14762  relexprng  14766  relexpfld  14769  relexpaddg  14773  invf  17489  sscres  17544  pgpssslw  19228  fislw  19239  frgpup1  19390  frgpup3lem  19392  dprdspan  19639  dprdz  19642  dprdf1o  19644  dprd2da  19654  ablfac1b  19682  lspsncmp  20387  lspsnne2  20389  lspsneq  20393  psgnghm2  20795  psrbaglesupp  21136  psrbaglesuppOLD  21137  psrbaglefi  21144  psrbaglefiOLD  21145  mplcoe5  21250  mplbas2  21252  ofco2  21609  toprntopon  22083  cncnpi  22438  hauscmplem  22566  iskgen2  22708  elqtop3  22863  qtoprest  22877  hmeores  22931  snfil  23024  uffixfr  23083  ustuqtop2  23403  tngngp2  23825  metnrmlem3  24033  volcn  24779  recnprss  25077  plyeq0  25381  uhgr3cyclex  28555  chsupsn  29784  chlejb1i  29847  atsseq  30718  disjeq1f  30921  ldgenpisys  32143  measxun2  32187  measssd  32192  measiuns  32194  pmeasmono  32300  eulerpartlemb  32344  bnj1143  32779  bnj1322  32811  funsseq  33751  madebdaylemlrcut  34088  opnbnd  34523  cldbnd  34524  fnemeet1  34564  bj-restuni  35277  bj-inexeqex  35334  bj-idreseq  35342  relowlpssretop  35544  pibt2  35597  ovoliunnfl  35828  voliunnfl  35830  volsupnfl  35831  heiborlem10  35987  smprngopr  36219  funALTVeq  36818  disjeq  36852  lshpcmp  37009  lsatcmp  37024  lsatcmp2  37025  lshpset2N  37140  paddasslem17  37857  pcl0bN  37944  pexmidALTN  37999  lcfrlem26  39589  lcfrlem36  39599  mapd0  39686  sn-iotassuni  40203  nacsfix  40541  minregex  41148  cbviuneq12df  41276  relexp0a  41331  relexpaddss  41333  frege124d  41376  k0004lem3  41766  dvconstbi  41959  ssin0  42610  icccncfext  43435  dvmptconst  43463  dvmptidg  43465  dvmulcncf  43473  dvdivcncf  43475  dirkercncflem2  43652  fourierdlem70  43724  fourierdlem71  43725  hoicvr  44093  ovnsubaddlem1  44115  ovnhoi  44148  hspdifhsp  44161  fcoreslem4  44571  seppsepf  46233  intubeu  46281  0setrec  46420