Theorem dmeqd 5918

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

Syntax hints:   → wi 4   = wceq 1536  dom cdm 5688

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1791  ax-4 1805  ax-5 1907  ax-6 1964  ax-7 2004  ax-8 2107  ax-9 2115  ax-ext 2705

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1539  df-fal 1549  df-ex 1776  df-sb 2062  df-clab 2712  df-cleq 2726  df-clel 2813  df-rab 3433  df-v 3479  df-dif 3965  df-un 3967  df-ss 3979  df-nul 4339  df-if 4531  df-sn 4631  df-pr 4633  df-op 4637  df-br 5148  df-dm 5698

This theorem is referenced by:  dmxpid  5943  rneq  5949  dmxpss  6192  dmsnopss  6235  dmsnsnsn  6241  f10d  6882  fndmin  7064  fninfp  7193  fndifnfp  7195  ovmpt3rabdm  7691  elxp4  7944  1stval  8014  fo1st  8032  f1stres  8036  bropopvvv  8113  bropfvvvv  8115  mpocurryd  8292  errn  8765  xpassen  9104  xpdom2  9105  oicl  9566  oif  9567  hartogslem1  9579  cantnfdm  9701  cantnfval  9705  cantnf0  9712  cantnfres  9714  cnfcomlem  9736  hsmexlem4  10466  hsmexlem5  10467  axdc3lem2  10488  ttukeylem3  10548  hashfun  14472  s1dmALT  14643  swrdval  14677  swrd0  14692  s2dmALT  14943  s4dom  14954  dmtrclfv  15053  relexpnndm  15076  relexpdmg  15077  relexpdmd  15079  relexpnnrn  15080  relexpfld  15084  relexpaddg  15088  shftdm  15106  rlim  15527  ramval  17041  isstruct2  17182  setsvalg  17199  setsdm  17203  prdsval  17501  homfeqbas  17740  invf  17815  dfiso2  17819  oppciso  17828  cicsym  17851  sscfn1  17864  sscfn2  17865  isssc  17867  rescval  17874  rescval2  17875  issubc  17885  issubc2  17886  cofuval  17932  resfval  17942  resfval2  17943  resf1st  17944  estrreslem2  18193  prfval  18254  lubdm  18408  glbdm  18421  joindm  18432  meetdm  18446  islat  18490  isclat  18557  oduclatb  18564  gsumvalx  18701  mndpsuppss  18790  cntzrcl  19357  f1omvdco2  19480  pmtrfrn  19490  symgsssg  19499  symgfisg  19500  symggen  19502  pmtrdifwrdellem3  19515  pmtrdifwrdel2lem1  19516  pmtrdifwrdel  19517  pmtrdifwrdel2  19518  psgnunilem1  19525  psgnunilem5  19526  psgnunilem2  19527  psgnunilem3  19528  psgneldm  19535  dmdprd  20032  dprdval  20037  dpjfval  20089  ablfaclem3  20121  cofipsgn  21628  elocv  21703  ishil  21755  dsmmval  21771  mpfrcl  22126  mamudm  22414  mavmuldm  22571  mavmul0g  22574  m1detdiag  22618  decpmatval0  22785  decpmatval  22786  pmatcollpw3lem  22804  iscnp2  23262  ptval  23593  ptcmplem2  24076  cnextfval  24085  tsmsval2  24153  ustbas2  24249  utopval  24256  tusval  24289  ucnval  24301  iscfilu  24312  psmetdmdm  24330  xmetdmdm  24360  blfvalps  24408  setsmstopn  24505  tmsval  24508  metuval  24577  tngtopn  24686  cfilfval  25311  caufval  25322  limcfval  25921  dvfval  25946  dvbsss  25951  perfdvf  25952  dvmptresicc  25965  dvn2bss  25980  dvnres  25981  dvcmul  25995  dvcmulf  25996  dvcj  26002  dvnfre  26004  dvexp  26005  dvmptres3  26008  dvmptcl  26011  dvmptadd  26012  dvmptmul  26013  dvmptres2  26014  dvmptcmul  26016  dvmptcj  26020  dvmptco  26024  rolle  26042  cmvth  26043  cmvthOLD  26044  mvth  26045  dvlip  26046  dvlipcn  26047  dvlip2  26048  c1liplem1  26049  dveq0  26053  dv11cn  26054  dvle  26060  dvivthlem1  26061  dvivth  26063  dvne0  26064  lhop1lem  26066  lhop2  26068  lhop  26069  dvcnvrelem1  26070  dvcvx  26073  dvfsumle  26074  dvfsumleOLD  26075  dvfsumge  26076  dvfsumabs  26077  dvmptrecl  26078  dvfsumlem2  26081  dvfsumlem2OLD  26082  itgsubstlem  26103  taylfval  26414  tayl0  26417  dvtaylp  26426  dvntaylp  26427  dvntaylp0  26428  taylthlem1  26429  taylthlem2  26430  taylthlem2OLD  26431  ulmdvlem1  26457  pserdv  26487  pige3ALT  26576  logtayl  26716  relogbf  26848  lgamgulmlem2  27087  nosupdm  27763  nosupbday  27764  nosupres  27766  nosupbnd1lem1  27767  nosupbnd1  27773  nosupbnd2  27775  noinfdm  27778  noinfbday  27779  noinfbnd1  27788  noinfbnd2  27790  perpln1  28732  isuhgr  29091  isushgr  29092  uhgreq12g  29096  isuhgrop  29101  uhgrun  29105  uhgrstrrepe  29109  isupgr  29115  upgrop  29125  isumgr  29126  upgr1e  29144  upgrun  29149  umgrun  29151  isuspgr  29183  isusgr  29184  isuspgrop  29192  isusgrop  29193  ausgrusgrb  29196  usgrstrrepe  29266  uspgr1e  29275  issubgr  29302  uhgrspansubgrlem  29321  usgrexi  29472  vtxdgfval  29499  vtxdeqd  29509  vtxdun  29513  1loopgrvd0  29536  1hevtxdg0  29537  1hevtxdg1  29538  umgr2v2e  29557  umgr2v2evd2  29559  ewlksfval  29633  wksfval  29641  wlkres  29702  wlkp1  29713  eupths  30228  eupthres  30243  trlsegvdeglem4  30251  trlsegvdeglem5  30252  grporndm  30538  hmoval  30838  gsumhashmul  33046  symgcom2  33086  symgcntz  33087  pmtrcnel2  33092  cycpmco2f1  33126  cycpmrn  33145  tocyccntz  33146  1arithidomlem2  33543  1arithidom  33544  minplyval  33712  smatrcl  33756  metidval  33850  pstmval  33855  prsssdm  33877  ordtrestNEW  33881  ofcfval  34078  ofcfval3  34082  brae  34221  braew  34222  faeval  34226  mbfmcst  34240  carsgval  34284  issibf  34314  sitmval  34330  0rrv  34432  dstrvprob  34452  fineqvac  35089  satfdm  35353  fmlafv  35364  fmla  35365  fmlasuc0  35368  satfdmfmla  35384  cnndvlem2  36520  bj-finsumval0  37267  cureq  37582  curf  37584  curunc  37588  sdclem2  37728  ismtyval  37786  isass  37832  isexid  37833  ismndo2  37860  exidreslem  37863  rngodm1dm2  37918  divrngcl  37943  isdrngo2  37944  cnvref4  38331  isopos  39161  isatl  39280  dibffval  41122  dibfval  41123  conrel2d  43653  iunrelexp0  43691  dmtrclfvRP  43719  rntrclfvRP  43720  neicvgbex  44101  dvsconst  44325  expgrowth  44330  fnlimfvre  45629  dvsinax  45868  dvcosax  45881  dvbdfbdioolem1  45883  itgsinexplem1  45909  itgcoscmulx  45924  dirkeritg  46057  dirkercncflem2  46059  fourierdlem60  46121  fourierdlem61  46122  fourierdlem74  46135  fourierdlem75  46136  fourierdlem80  46141  fourierdlem94  46155  fourierdlem103  46164  fourierdlem104  46165  fourierdlem113  46174  dmvon  46561  ovnovollem1  46611  smflimlem3  46728  smflimlem4  46729  smflim  46732  smflim2  46761  smfpimcc  46763  smflimmpt  46765  smfsuplem2  46767  smfsuplem3  46768  smfsup  46769  smfsupmpt  46770  smfinflem  46772  smfinf  46773  smfinfmpt  46774  smflimsuplem1  46775  smflimsuplem2  46776  smflimsuplem3  46777  smflimsuplem4  46778  smflimsuplem7  46781  smflimsup  46783  smflimsupmpt  46784  smfliminf  46786  smfliminfmpt  46787  dfateq12d  47075  isubgruhgr  47791  grimidvtxedg  47813  ushggricedg  47833  isubgrgrim  47834  stgrusgra  47861  gpgusgra  47946  upwlksfval  47978  lubeldm2d  48754  glbeldm2d  48755  glbprlem  48761  isclatd  48771