Theorem dmeqd 5912

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

Syntax hints:   → wi 4   = wceq 1533  dom cdm 5682

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1905  ax-6 1963  ax-7 2003  ax-8 2100  ax-9 2108  ax-ext 2699

This theorem depends on definitions:  df-bi 206  df-an 395  df-or 846  df-3an 1086  df-tru 1536  df-fal 1546  df-ex 1774  df-sb 2060  df-clab 2706  df-cleq 2720  df-clel 2806  df-rab 3431  df-v 3475  df-dif 3952  df-un 3954  df-in 3956  df-ss 3966  df-nul 4327  df-if 4533  df-sn 4633  df-pr 4635  df-op 4639  df-br 5153  df-dm 5692

This theorem is referenced by:  dmxpid  5936  rneq  5942  dmxpss  6180  dmsnopss  6223  dmsnsnsn  6229  f10d  6878  fndmin  7059  fninfp  7189  fndifnfp  7191  ovmpt3rabdm  7686  elxp4  7936  1stval  8001  fo1st  8019  f1stres  8023  bropopvvv  8101  bropfvvvv  8103  mpocurryd  8281  errn  8753  xpassen  9097  xpdom2  9098  oicl  9560  oif  9561  hartogslem1  9573  cantnfdm  9695  cantnfval  9699  cantnf0  9706  cantnfres  9708  cnfcomlem  9730  hsmexlem4  10460  hsmexlem5  10461  axdc3lem2  10482  ttukeylem3  10542  hashfun  14436  s1dmALT  14599  swrdval  14633  swrd0  14648  s2dmALT  14899  s4dom  14910  dmtrclfv  15005  relexpnndm  15028  relexpdmg  15029  relexpdmd  15031  relexpnnrn  15032  relexpfld  15036  relexpaddg  15040  shftdm  15058  rlim  15479  ramval  16984  isstruct2  17125  setsvalg  17142  setsdm  17146  prdsval  17444  homfeqbas  17683  invf  17758  dfiso2  17762  oppciso  17771  cicsym  17794  sscfn1  17807  sscfn2  17808  isssc  17810  rescval  17817  rescval2  17818  issubc  17828  issubc2  17829  cofuval  17875  resfval  17885  resfval2  17886  resf1st  17887  estrreslem2  18136  prfval  18197  lubdm  18350  glbdm  18363  joindm  18374  meetdm  18388  islat  18432  isclat  18499  oduclatb  18506  gsumvalx  18643  cntzrcl  19285  f1omvdco2  19410  pmtrfrn  19420  symgsssg  19429  symgfisg  19430  symggen  19432  pmtrdifwrdellem3  19445  pmtrdifwrdel2lem1  19446  pmtrdifwrdel  19447  pmtrdifwrdel2  19448  psgnunilem1  19455  psgnunilem5  19456  psgnunilem2  19457  psgnunilem3  19458  psgneldm  19465  dmdprd  19962  dprdval  19967  dpjfval  20019  ablfaclem3  20051  cofipsgn  21532  elocv  21607  ishil  21659  dsmmval  21675  mpfrcl  22038  mamudm  22310  mavmuldm  22472  mavmul0g  22475  m1detdiag  22519  decpmatval0  22686  decpmatval  22687  pmatcollpw3lem  22705  iscnp2  23163  ptval  23494  ptcmplem2  23977  cnextfval  23986  tsmsval2  24054  ustbas2  24150  utopval  24157  tusval  24190  ucnval  24202  iscfilu  24213  psmetdmdm  24231  xmetdmdm  24261  blfvalps  24309  setsmstopn  24406  tmsval  24409  metuval  24478  tngtopn  24587  cfilfval  25212  caufval  25223  limcfval  25821  dvfval  25846  dvbsss  25851  perfdvf  25852  dvmptresicc  25865  dvn2bss  25880  dvnres  25881  dvcmul  25895  dvcmulf  25896  dvcj  25902  dvnfre  25904  dvexp  25905  dvmptres3  25908  dvmptcl  25911  dvmptadd  25912  dvmptmul  25913  dvmptres2  25914  dvmptcmul  25916  dvmptcj  25920  dvmptco  25924  rolle  25942  cmvth  25943  cmvthOLD  25944  mvth  25945  dvlip  25946  dvlipcn  25947  dvlip2  25948  c1liplem1  25949  dveq0  25953  dv11cn  25954  dvle  25960  dvivthlem1  25961  dvivth  25963  dvne0  25964  lhop1lem  25966  lhop2  25968  lhop  25969  dvcnvrelem1  25970  dvcvx  25973  dvfsumle  25974  dvfsumleOLD  25975  dvfsumge  25976  dvfsumabs  25977  dvmptrecl  25978  dvfsumlem2  25981  dvfsumlem2OLD  25982  itgsubstlem  26003  taylfval  26313  tayl0  26316  dvtaylp  26325  dvntaylp  26326  dvntaylp0  26327  taylthlem1  26328  taylthlem2  26329  taylthlem2OLD  26330  ulmdvlem1  26356  pserdv  26386  pige3ALT  26474  logtayl  26614  relogbf  26743  lgamgulmlem2  26982  nosupdm  27657  nosupbday  27658  nosupres  27660  nosupbnd1lem1  27661  nosupbnd1  27667  nosupbnd2  27669  noinfdm  27672  noinfbday  27673  noinfbnd1  27682  noinfbnd2  27684  perpln1  28534  isuhgr  28893  isushgr  28894  uhgreq12g  28898  isuhgrop  28903  uhgrun  28907  uhgrstrrepe  28911  isupgr  28917  upgrop  28927  isumgr  28928  upgr1e  28946  upgrun  28951  umgrun  28953  isuspgr  28985  isusgr  28986  isuspgrop  28994  isusgrop  28995  ausgrusgrb  28998  usgrstrrepe  29068  uspgr1e  29077  usgrexmpl  29096  issubgr  29104  uhgrspansubgrlem  29123  usgrexi  29274  vtxdgfval  29301  vtxdeqd  29311  vtxdun  29315  1loopgrvd0  29338  1hevtxdg0  29339  1hevtxdg1  29340  umgr2v2e  29359  umgr2v2evd2  29361  ewlksfval  29435  wksfval  29443  wlkres  29504  wlkp1  29515  eupths  30030  eupthres  30045  trlsegvdeglem4  30053  trlsegvdeglem5  30054  grporndm  30340  hmoval  30640  gsumhashmul  32791  symgcom2  32828  symgcntz  32829  pmtrcnel2  32834  cycpmco2f1  32866  cycpmrn  32885  tocyccntz  32886  minplyval  33409  smatrcl  33430  metidval  33524  pstmval  33529  prsssdm  33551  ordtrestNEW  33555  ofcfval  33750  ofcfval3  33754  brae  33893  braew  33894  faeval  33898  mbfmcst  33912  carsgval  33956  issibf  33986  sitmval  34002  0rrv  34104  dstrvprob  34124  fineqvac  34750  satfdm  35012  fmlafv  35023  fmla  35024  fmlasuc0  35027  satfdmfmla  35043  cnndvlem2  36046  bj-finsumval0  36797  cureq  37102  curf  37104  curunc  37108  sdclem2  37248  ismtyval  37306  isass  37352  isexid  37353  ismndo2  37380  exidreslem  37383  rngodm1dm2  37438  divrngcl  37463  isdrngo2  37464  cnvref4  37854  isopos  38684  isatl  38803  dibffval  40645  dibfval  40646  conrel2d  43125  iunrelexp0  43163  dmtrclfvRP  43191  rntrclfvRP  43192  neicvgbex  43573  dvsconst  43798  expgrowth  43803  fnlimfvre  45091  dvsinax  45330  dvcosax  45343  dvbdfbdioolem1  45345  itgsinexplem1  45371  itgcoscmulx  45386  dirkeritg  45519  dirkercncflem2  45521  fourierdlem60  45583  fourierdlem61  45584  fourierdlem74  45597  fourierdlem75  45598  fourierdlem80  45603  fourierdlem94  45617  fourierdlem103  45626  fourierdlem104  45627  fourierdlem113  45636  dmvon  46023  ovnovollem1  46073  smflimlem3  46190  smflimlem4  46191  smflim  46194  smflim2  46223  smfpimcc  46225  smflimmpt  46227  smfsuplem2  46229  smfsuplem3  46230  smfsup  46231  smfsupmpt  46232  smfinflem  46234  smfinf  46235  smfinfmpt  46236  smflimsuplem1  46237  smflimsuplem2  46238  smflimsuplem3  46239  smflimsuplem4  46240  smflimsuplem7  46243  smflimsup  46245  smflimsupmpt  46246  smfliminf  46248  smfliminfmpt  46249  dfateq12d  46535  isubgruhgr  47230  grimidvtxedg  47252  ushggricedg  47271  upwlksfval  47275  mndpsuppss  47513  lubeldm2d  48055  glbeldm2d  48056  glbprlem  48062  isclatd  48072