Theorem eqimss 3976

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

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

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 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 397  df-tru 1542  df-ex 1783  df-sb 2068  df-clab 2716  df-cleq 2730  df-clel 2816  df-v 3431  df-in 3893  df-ss 3903

This theorem is referenced by:  eqimss2  3977  sspss  4033  uneqin  4212  difn0  4298  ssdisj  4393  uneqdifeq  4423  pweq  4549  pwpw0  4746  ssprsseq  4758  sssn  4759  snsspw  4775  pwsnOLD  4832  unieq  4850  unissint  4903  pwpwssunieq  5032  elpwuni  5033  disjeq2  5042  disjeq1  5045  pwne  5271  pwssun  5480  poeq2  5502  freq2  5555  seeq1  5556  seeq2  5557  frsn  5669  dmxpss  6067  xp11  6071  dmsnopss  6110  trsucss  6344  suc11  6362  iotassuni  6405  funeq  6446  fnresdm  6543  fssxp  6620  ffdm  6622  fcoi1  6640  fof  6680  dff1o2  6713  fvmptss  6879  fvmptss2  6892  funressn  7023  dff1o6  7139  sucexeloni  7648  suceloniOLD  7650  tposeq  8031  tfrlem11  8206  oewordi  8409  oewordri  8410  dffi3  9177  cantnfle  9416  cantnflem2  9435  r1ord3g  9547  rankeq0b  9628  rankxplim3  9649  carddom2  9745  cflm  10016  cfsuc  10023  isf32lem2  10120  axdc3lem2  10217  ttukeylem5  10279  tsksuc  10528  fsuppmapnn0fiublem  13720  fsuppmapnn0fiub  13721  xptrrel  14701  relexpnndm  14762  relexpdmg  14763  relexprng  14767  relexpfld  14770  relexpaddg  14774  invf  17490  sscres  17545  pgpssslw  19229  fislw  19240  frgpup1  19391  frgpup3lem  19393  dprdspan  19640  dprdz  19643  dprdf1o  19645  dprd2da  19655  ablfac1b  19683  lspsncmp  20388  lspsnne2  20390  lspsneq  20394  psgnghm2  20796  psrbaglesupp  21137  psrbaglesuppOLD  21138  psrbaglefi  21145  psrbaglefiOLD  21146  mplcoe5  21251  mplbas2  21253  ofco2  21610  toprntopon  22084  cncnpi  22439  hauscmplem  22567  iskgen2  22709  elqtop3  22864  qtoprest  22878  hmeores  22932  snfil  23025  uffixfr  23084  ustuqtop2  23404  tngngp2  23826  metnrmlem3  24034  volcn  24780  recnprss  25078  plyeq0  25382  uhgr3cyclex  28554  chsupsn  29783  chlejb1i  29846  atsseq  30717  disjeq1f  30920  ldgenpisys  32142  measxun2  32186  measssd  32191  measiuns  32193  pmeasmono  32299  eulerpartlemb  32343  bnj1143  32778  bnj1322  32810  funsseq  33750  madebdaylemlrcut  34087  opnbnd  34522  cldbnd  34523  fnemeet1  34563  bj-restuni  35276  bj-inexeqex  35333  bj-idreseq  35341  relowlpssretop  35543  pibt2  35596  ovoliunnfl  35827  voliunnfl  35829  volsupnfl  35830  heiborlem10  35986  smprngopr  36218  funALTVeq  36819  disjeq  36853  lshpcmp  37010  lsatcmp  37025  lsatcmp2  37026  lshpset2N  37141  paddasslem17  37858  pcl0bN  37945  pexmidALTN  38000  lcfrlem26  39590  lcfrlem36  39600  mapd0  39687  sn-iotassuni  40204  nacsfix  40542  cbviuneq12df  41250  relexp0a  41305  relexpaddss  41307  frege124d  41350  k0004lem3  41740  dvconstbi  41933  ssin0  42584  icccncfext  43409  dvmptconst  43437  dvmptidg  43439  dvmulcncf  43447  dvdivcncf  43449  dirkercncflem2  43626  fourierdlem70  43698  fourierdlem71  43699  hoicvr  44067  ovnsubaddlem1  44089  ovnhoi  44122  hspdifhsp  44135  fcoreslem4  44538  seppsepf  46200  intubeu  46248  0setrec  46387