Theorem dmeqd 5869

Description: Equality deduction for domain. (Contributed by NM, 4-Mar-2004.)

Hypothesis

Ref	Expression
dmeqd.1	⊢ (𝜑 → 𝐴 = 𝐵)

Assertion

Ref	Expression
dmeqd	⊢ (𝜑 → dom 𝐴 = dom 𝐵)

Proof of Theorem dmeqd

Step	Hyp	Ref	Expression
1		dmeqd.1	. 2 ⊢ (𝜑 → 𝐴 = 𝐵)
2		dmeq 5867	. 2 ⊢ (𝐴 = 𝐵 → dom 𝐴 = dom 𝐵)
3	1, 2	syl 17	1 ⊢ (𝜑 → dom 𝐴 = dom 𝐵)

Syntax hints:   → wi 4   = wceq 1540  dom cdm 5638

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-rab 3406  df-v 3449  df-dif 3917  df-un 3919  df-ss 3931  df-nul 4297  df-if 4489  df-sn 4590  df-pr 4592  df-op 4596  df-br 5108  df-dm 5648

This theorem is referenced by:  dmxpid  5894  rneq  5900  dmxpss  6144  dmsnopss  6187  dmsnsnsn  6193  f10d  6834  fndmin  7017  fninfp  7148  fndifnfp  7150  ovmpt3rabdm  7648  elxp4  7898  1stval  7970  fo1st  7988  f1stres  7992  bropopvvv  8069  bropfvvvv  8071  mpocurryd  8248  errn  8693  xpassen  9035  xpdom2  9036  oicl  9482  oif  9483  hartogslem1  9495  cantnfdm  9617  cantnfval  9621  cantnf0  9628  cantnfres  9630  cnfcomlem  9652  hsmexlem4  10382  hsmexlem5  10383  axdc3lem2  10404  ttukeylem3  10464  hashfun  14402  s1dmALT  14574  swrdval  14608  swrd0  14623  s2dmALT  14874  s4dom  14885  dmtrclfv  14984  relexpnndm  15007  relexpdmg  15008  relexpdmd  15010  relexpnnrn  15011  relexpfld  15015  relexpaddg  15019  shftdm  15037  rlim  15461  ramval  16979  isstruct2  17119  setsvalg  17136  setsdm  17140  prdsval  17418  homfeqbas  17657  invf  17730  dfiso2  17734  oppciso  17743  cicsym  17766  sscfn1  17779  sscfn2  17780  isssc  17782  rescval  17789  rescval2  17790  issubc  17797  issubc2  17798  cofuval  17844  resfval  17854  resfval2  17855  resf1st  17856  estrreslem2  18099  prfval  18160  lubdm  18310  glbdm  18323  joindm  18334  meetdm  18348  islat  18392  isclat  18459  oduclatb  18466  gsumvalx  18603  mndpsuppss  18692  cntzrcl  19259  f1omvdco2  19378  pmtrfrn  19388  symgsssg  19397  symgfisg  19398  symggen  19400  pmtrdifwrdellem3  19413  pmtrdifwrdel2lem1  19414  pmtrdifwrdel  19415  pmtrdifwrdel2  19416  psgnunilem1  19423  psgnunilem5  19424  psgnunilem2  19425  psgnunilem3  19426  psgneldm  19433  dmdprd  19930  dprdval  19935  dpjfval  19987  ablfaclem3  20019  cofipsgn  21502  elocv  21577  ishil  21627  dsmmval  21643  mpfrcl  21992  mamudm  22282  mavmuldm  22437  mavmul0g  22440  m1detdiag  22484  decpmatval0  22651  decpmatval  22652  pmatcollpw3lem  22670  iscnp2  23126  ptval  23457  ptcmplem2  23940  cnextfval  23949  tsmsval2  24017  ustbas2  24113  utopval  24120  tusval  24153  ucnval  24164  iscfilu  24175  psmetdmdm  24193  xmetdmdm  24223  blfvalps  24271  setsmstopn  24366  tmsval  24369  metuval  24437  tngtopn  24538  cfilfval  25164  caufval  25175  limcfval  25773  dvfval  25798  dvbsss  25803  perfdvf  25804  dvmptresicc  25817  dvn2bss  25832  dvnres  25833  dvcmul  25847  dvcmulf  25848  dvcj  25854  dvnfre  25856  dvexp  25857  dvmptres3  25860  dvmptcl  25863  dvmptadd  25864  dvmptmul  25865  dvmptres2  25866  dvmptcmul  25868  dvmptcj  25872  dvmptco  25876  rolle  25894  cmvth  25895  cmvthOLD  25896  mvth  25897  dvlip  25898  dvlipcn  25899  dvlip2  25900  c1liplem1  25901  dveq0  25905  dv11cn  25906  dvle  25912  dvivthlem1  25913  dvivth  25915  dvne0  25916  lhop1lem  25918  lhop2  25920  lhop  25921  dvcnvrelem1  25922  dvcvx  25925  dvfsumle  25926  dvfsumleOLD  25927  dvfsumge  25928  dvfsumabs  25929  dvmptrecl  25930  dvfsumlem2  25933  dvfsumlem2OLD  25934  itgsubstlem  25955  taylfval  26266  tayl0  26269  dvtaylp  26278  dvntaylp  26279  dvntaylp0  26280  taylthlem1  26281  taylthlem2  26282  taylthlem2OLD  26283  ulmdvlem1  26309  pserdv  26339  pige3ALT  26429  logtayl  26569  relogbf  26701  lgamgulmlem2  26940  nosupdm  27616  nosupbday  27617  nosupres  27619  nosupbnd1lem1  27620  nosupbnd1  27626  nosupbnd2  27628  noinfdm  27631  noinfbday  27632  noinfbnd1  27641  noinfbnd2  27643  perpln1  28637  isuhgr  28987  isushgr  28988  uhgreq12g  28992  isuhgrop  28997  uhgrun  29001  uhgrstrrepe  29005  isupgr  29011  upgrop  29021  isumgr  29022  upgr1e  29040  upgrun  29045  umgrun  29047  isuspgr  29079  isusgr  29080  isuspgrop  29088  isusgrop  29089  ausgrusgrb  29092  usgrstrrepe  29162  uspgr1e  29171  issubgr  29198  uhgrspansubgrlem  29217  usgrexi  29368  vtxdgfval  29395  vtxdeqd  29405  vtxdun  29409  1loopgrvd0  29432  1hevtxdg0  29433  1hevtxdg1  29434  umgr2v2e  29453  umgr2v2evd2  29455  ewlksfval  29529  wksfval  29537  wlkres  29598  wlkp1  29609  eupths  30129  eupthres  30144  trlsegvdeglem4  30152  trlsegvdeglem5  30153  grporndm  30439  hmoval  30739  gsumhashmul  33001  symgcom2  33041  symgcntz  33042  pmtrcnel2  33047  cycpmco2f1  33081  cycpmrn  33100  tocyccntz  33101  fxpval  33122  fxpgaval  33124  1arithidomlem2  33507  1arithidom  33508  minplyval  33695  smatrcl  33786  metidval  33880  pstmval  33885  prsssdm  33907  ordtrestNEW  33911  ofcfval  34088  ofcfval3  34092  brae  34231  braew  34232  faeval  34236  mbfmcst  34250  carsgval  34294  issibf  34324  sitmval  34340  0rrv  34442  dstrvprob  34463  fineqvac  35087  satfdm  35356  fmlafv  35367  fmla  35368  fmlasuc0  35371  satfdmfmla  35387  cnndvlem2  36526  bj-finsumval0  37273  cureq  37590  curf  37592  curunc  37596  sdclem2  37736  ismtyval  37794  isass  37840  isexid  37841  ismndo2  37868  exidreslem  37871  rngodm1dm2  37926  divrngcl  37951  isdrngo2  37952  cnvref4  38332  isopos  39173  isatl  39292  dibffval  41134  dibfval  41135  conrel2d  43653  iunrelexp0  43691  dmtrclfvRP  43719  rntrclfvRP  43720  neicvgbex  44101  dvsconst  44319  expgrowth  44324  fnlimfvre  45672  dvsinax  45911  dvcosax  45924  dvbdfbdioolem1  45926  itgsinexplem1  45952  itgcoscmulx  45967  dirkeritg  46100  dirkercncflem2  46102  fourierdlem60  46164  fourierdlem61  46165  fourierdlem74  46178  fourierdlem75  46179  fourierdlem80  46184  fourierdlem94  46198  fourierdlem103  46207  fourierdlem104  46208  fourierdlem113  46217  dmvon  46604  ovnovollem1  46654  smflimlem3  46771  smflimlem4  46772  smflim  46775  smflim2  46804  smfpimcc  46806  smflimmpt  46808  smfsuplem2  46810  smfsuplem3  46811  smfsup  46812  smfsupmpt  46813  smfinflem  46815  smfinf  46816  smfinfmpt  46817  smflimsuplem1  46818  smflimsuplem2  46819  smflimsuplem3  46820  smflimsuplem4  46821  smflimsuplem7  46824  smflimsup  46826  smflimsupmpt  46827  smfliminf  46829  smfliminfmpt  46830  dfateq12d  47127  isubgruhgr  47868  grimidvtxedg  47885  ushggricedg  47927  isubgrgrim  47929  stgrusgra  47958  gpgiedgdmel  48040  gpgusgra  48048  upwlksfval  48123  dmrnxp  48825  lubeldm2d  48946  glbeldm2d  48947  glbprlem  48953  isclatd  48971  isopropdlem  49029  dmdm  49042  infsubc2  49050  infsubc2d  49051  oppfvalg  49115  reldmprcof1  49370  reldmprcof2  49371  dfinito4  49490  reldmlan2  49606  reldmran2  49607  termolmd  49659