Theorem eqimss 3973

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

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2110  ax-9 2118  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 396  df-tru 1542  df-ex 1784  df-sb 2069  df-clab 2716  df-cleq 2730  df-clel 2817  df-v 3424  df-in 3890  df-ss 3900

This theorem is referenced by:  eqimss2  3974  sspss  4030  uneqin  4209  difn0  4295  ssdisj  4390  uneqdifeq  4420  pweq  4546  pwpw0  4743  ssprsseq  4755  sssn  4756  snsspw  4772  pwsnOLD  4829  unieq  4847  unissint  4900  pwpwssunieq  5029  elpwuni  5030  disjeq2  5039  disjeq1  5042  pwne  5268  pwssun  5476  poeq2  5498  freq2  5551  seeq1  5552  seeq2  5553  frsn  5665  dmxpss  6063  xp11  6067  dmsnopss  6106  trsucss  6336  suc11  6354  iotassuni  6397  funeq  6438  fnresdm  6535  fssxp  6612  ffdm  6614  fcoi1  6632  fof  6672  dff1o2  6705  fvmptss  6869  fvmptss2  6882  funressn  7013  dff1o6  7128  suceloni  7635  tposeq  8015  tfrlem11  8190  oewordi  8384  oewordri  8385  dffi3  9120  cantnfle  9359  cantnflem2  9378  r1ord3g  9468  rankeq0b  9549  rankxplim3  9570  carddom2  9666  cflm  9937  cfsuc  9944  isf32lem2  10041  axdc3lem2  10138  ttukeylem5  10200  tsksuc  10449  fsuppmapnn0fiublem  13638  fsuppmapnn0fiub  13639  xptrrel  14619  relexpnndm  14680  relexpdmg  14681  relexprng  14685  relexpfld  14688  relexpaddg  14692  invf  17397  sscres  17452  pgpssslw  19134  fislw  19145  frgpup1  19296  frgpup3lem  19298  dprdspan  19545  dprdz  19548  dprdf1o  19550  dprd2da  19560  ablfac1b  19588  lspsncmp  20293  lspsnne2  20295  lspsneq  20299  psgnghm2  20698  psrbaglesupp  21037  psrbaglesuppOLD  21038  psrbaglefi  21045  psrbaglefiOLD  21046  mplcoe5  21151  mplbas2  21153  ofco2  21508  toprntopon  21982  cncnpi  22337  hauscmplem  22465  iskgen2  22607  elqtop3  22762  qtoprest  22776  hmeores  22830  snfil  22923  uffixfr  22982  ustuqtop2  23302  tngngp2  23722  metnrmlem3  23930  volcn  24675  recnprss  24973  plyeq0  25277  uhgr3cyclex  28447  chsupsn  29676  chlejb1i  29739  atsseq  30610  disjeq1f  30813  ldgenpisys  32034  measxun2  32078  measssd  32083  measiuns  32085  pmeasmono  32191  eulerpartlemb  32235  bnj1143  32670  bnj1322  32702  funsseq  33648  madebdaylemlrcut  34006  opnbnd  34441  cldbnd  34442  fnemeet1  34482  bj-restuni  35195  bj-inexeqex  35252  bj-idreseq  35260  relowlpssretop  35462  pibt2  35515  ovoliunnfl  35746  voliunnfl  35748  volsupnfl  35749  heiborlem10  35905  smprngopr  36137  funALTVeq  36738  disjeq  36772  lshpcmp  36929  lsatcmp  36944  lsatcmp2  36945  lshpset2N  37060  paddasslem17  37777  pcl0bN  37864  pexmidALTN  37919  lcfrlem26  39509  lcfrlem36  39519  mapd0  39606  sn-iotassuni  40122  nacsfix  40450  cbviuneq12df  41158  relexp0a  41213  relexpaddss  41215  frege124d  41258  k0004lem3  41648  dvconstbi  41841  ssin0  42492  icccncfext  43318  dvmptconst  43346  dvmptidg  43348  dvmulcncf  43356  dvdivcncf  43358  dirkercncflem2  43535  fourierdlem70  43607  fourierdlem71  43608  hoicvr  43976  ovnsubaddlem1  43998  ovnhoi  44031  hspdifhsp  44044  fcoreslem4  44447  seppsepf  46110  intubeu  46158  0setrec  46295