Theorem dmeqd 5895

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 5893	. 2 ⊢ (𝐴 = 𝐵 → dom 𝐴 = dom 𝐵)
3	1, 2	syl 18	1 ⊢ (𝜑 → dom 𝐴 = dom 𝐵)

Syntax hints:   → wi 4   = wceq 1570  dom cdm 5661

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-8 2145  ax-9 2153  ax-ext 2735

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1810  df-sb 2097  df-clab 2742  df-cleq 2755  df-clel 2838  df-rab 3417  df-v 3457  df-dif 3908  df-un 3910  df-ss 3922  df-nul 4287  df-if 4488  df-sn 4590  df-pr 4592  df-op 4596  df-br 5110  df-dm 5671

This theorem is referenced by:  dmxpid  5920  rneq  5926  dmxpss  6169  dmsnopss  6215  dmsnsnsn  6221  f10d  6855  fndmin  7040  fninfp  7172  fndifnfp  7174  ovmpt3rabdm  7669  elxp4  7915  1stval  7984  fo1st  8002  f1stres  8006  bropopvvv  8081  bropfvvvv  8083  mpocurryd  8261  errn  8713  xpassen  9055  xpdom2  9056  oicl  9487  oif  9488  hartogslem1  9500  cantnfdm  9629  cantnfval  9633  cantnf0  9640  cantnfres  9642  cnfcomlem  9664  hsmexlem4  10408  hsmexlem5  10409  axdc3lem2  10430  ttukeylem3  10490  hashfun  14470  s1dmALT  14643  swrdval  14677  swrd0  14692  s2dmALT  14941  s4dom  14952  dmtrclfv  15051  relexpnndm  15074  relexpdmg  15075  relexpdmd  15077  relexpnnrn  15078  relexpfld  15082  relexpaddg  15086  shftdm  15104  rlim  15542  ramval  17063  isstruct2  17204  setsvalg  17221  setsdm  17225  prdsval  17503  homfeqbas  17747  invf  17820  dfiso2  17824  oppciso  17833  cicsym  17856  sscfn1  17869  sscfn2  17870  isssc  17872  rescval  17879  rescval2  17880  issubc  17887  issubc2  17888  cofuval  17934  resfval  17944  resfval2  17945  resf1st  17946  estrreslem2  18189  prfval  18250  lubdm  18400  glbdm  18413  joindm  18424  meetdm  18438  islat  18484  isclat  18551  oduclatb  18558  gsumvalx  18729  mndpsuppss  18818  cntzrcl  19392  f1omvdco2  19513  pmtrfrn  19523  symgsssg  19532  symgfisg  19533  symggen  19535  pmtrdifwrdellem3  19548  pmtrdifwrdel2lem1  19549  pmtrdifwrdel  19550  pmtrdifwrdel2  19551  psgnunilem1  19558  psgnunilem5  19559  psgnunilem2  19560  psgnunilem3  19561  psgneldm  19568  dmdprd  20065  dprdval  20070  dpjfval  20122  ablfaclem3  20154  cofipsgn  21743  elocv  21818  ishil  21868  dsmmval  21884  mpfrcl  22236  mamudm  22552  mavmuldm  22707  mavmul0g  22710  m1detdiag  22754  decpmatval0  22921  decpmatval  22922  pmatcollpw3lem  22940  iscnp2  23396  ptval  23727  ptcmplem2  24210  cnextfval  24219  tsmsval2  24287  ustbas2  24382  utopval  24389  tusval  24422  ucnval  24433  iscfilu  24444  psmetdmdm  24462  xmetdmdm  24492  blfvalps  24540  setsmstopn  24635  tmsval  24638  metuval  24706  tngtopn  24807  cfilfval  25423  caufval  25434  limcfval  26031  dvfval  26056  dvbsss  26061  perfdvf  26062  dvmptresicc  26075  dvn2bss  26089  dvnres  26090  dvcmul  26103  dvcmulf  26104  dvcj  26109  dvnfre  26111  dvexp  26112  dvmptres3  26115  dvmptcl  26118  dvmptadd  26119  dvmptmul  26120  dvmptres2  26121  dvmptcmul  26123  dvmptcj  26127  dvmptco  26131  rolle  26149  cmvth  26150  mvth  26151  dvlip  26152  dvlipcn  26153  dvlip2  26154  c1liplem1  26155  dveq0  26159  dv11cn  26160  dvle  26166  dvivthlem1  26167  dvivth  26169  dvne0  26170  lhop1lem  26172  lhop2  26174  lhop  26175  dvcnvrelem1  26176  dvcvx  26179  dvfsumle  26180  dvfsumge  26181  dvfsumabs  26182  dvmptrecl  26183  dvfsumlem2  26186  itgsubstlem  26207  taylfval  26522  tayl0  26525  dvtaylp  26533  dvntaylp  26534  dvntaylp0  26535  taylthlem1  26536  taylthlem2  26537  ulmdvlem1  26563  pserdv  26592  pige3ALT  26685  logtayl  26825  relogbf  26956  lgamgulmlem2  27194  nosupdm  27868  nosupbday  27869  nosupres  27871  nosupbnd1lem1  27872  nosupbnd1  27878  nosupbnd2  27880  noinfdm  27883  noinfbday  27884  noinfbnd1  27893  noinfbnd2  27895  perpln1  28990  isuhgr  29410  isushgr  29411  uhgreq12g  29415  isuhgrop  29420  uhgrun  29424  uhgrstrrepe  29428  isupgr  29434  upgrop  29444  isumgr  29445  upgr1e  29463  upgrun  29468  umgrun  29470  isuspgr  29502  isusgr  29503  isuspgrop  29511  isusgrop  29512  ausgrusgrb  29515  usgrstrrepe  29585  uspgr1e  29594  issubgr  29621  uhgrspansubgrlem  29640  usgrexi  29791  vtxdgfval  29817  vtxdeqd  29827  vtxdun  29831  1loopgrvd0  29854  1hevtxdg0  29855  1hevtxdg1  29856  umgr2v2e  29875  umgr2v2evd2  29877  ewlksfval  29951  wksfval  29959  wlkres  30018  wlkp1  30029  eupths  30551  eupthres  30566  trlsegvdeglem4  30574  trlsegvdeglem5  30575  grporndm  30862  hmoval  31162  gsumhashmul  33387  symgcom2  33404  symgcntz  33405  pmtrcnel2  33410  cycpmco2f1  33444  cycpmrn  33463  tocyccntz  33464  fxpval  33485  fxpgaval  33487  1arithidomlem2  33826  1arithidom  33827  minplyval  34095  smatrcl  34186  metidval  34280  pstmval  34285  prsssdm  34307  ordtrestNEW  34311  ofcfval  34488  ofcfval3  34492  brae  34631  braew  34632  faeval  34636  mbfmcst  34649  carsgval  34693  issibf  34723  sitmval  34739  0rrv  34841  dstrvprob  34862  fineqvac  35529  satfdm  35861  fmlafv  35872  fmla  35873  fmlasuc0  35876  satfdmfmla  35892  cnndvlem2  37127  bj-finsumval0  37929  cureq  38247  curf  38249  curunc  38253  sdclem2  38393  ismtyval  38451  isass  38497  isexid  38498  ismndo2  38525  exidreslem  38528  rngodm1dm2  38583  divrngcl  38608  isdrngo2  38609  cnvref4  38999  isopos  39954  isatl  40073  dibffval  41914  dibfval  41915  conrel2d  44390  iunrelexp0  44428  dmtrclfvRP  44456  rntrclfvRP  44457  neicvgbex  44838  dvsconst  45040  expgrowth  45045  fnlimfvre  46388  dvsinax  46627  dvcosax  46640  dvbdfbdioolem1  46642  itgsinexplem1  46668  itgcoscmulx  46683  dirkeritg  46816  dirkercncflem2  46818  fourierdlem60  46880  fourierdlem61  46881  fourierdlem74  46894  fourierdlem75  46895  fourierdlem80  46900  fourierdlem94  46914  fourierdlem103  46923  fourierdlem104  46924  fourierdlem113  46933  dmvon  47320  ovnovollem1  47370  smflimlem3  47487  smflimlem4  47488  smflim  47491  smflim2  47520  smfpimcc  47522  smflimmpt  47524  smfsuplem2  47526  smfsuplem3  47527  smfsup  47528  smfsupmpt  47529  smfinflem  47531  smfinf  47532  smfinfmpt  47533  smflimsuplem1  47534  smflimsuplem2  47535  smflimsuplem3  47536  smflimsuplem4  47537  smflimsuplem7  47540  smflimsup  47542  smflimsupmpt  47543  smfliminf  47545  smfliminfmpt  47546  dfateq12d  47863  isubgruhgr  48633  grimidvtxedg  48650  ushggricedg  48692  isubgrgrim  48694  stgrusgra  48724  gpgiedgdmel  48814  gpgusgra  48822  upwlksfval  48900  dmrnxp  49615  lubeldm2d  49736  glbeldm2d  49737  glbprlem  49743  isclatd  49761  isopropdlem  49818  dmdm  49831  infsubc2  49839  infsubc2d  49840  oppfvalg  49904  reldmprcof1  50159  reldmprcof2  50160  dfinito4  50279  reldmlan2  50395  reldmran2  50396  termolmd  50448