Theorem dmeqd 5847

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

Syntax hints:   → wi 4   = wceq 1547  dom cdm 5618

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-ext 2711

This theorem depends on definitions:  df-bi 208  df-an 397  df-or 854  df-3an 1094  df-tru 1550  df-fal 1560  df-ex 1787  df-sb 2074  df-clab 2718  df-cleq 2731  df-clel 2814  df-rab 3392  df-v 3433  df-dif 3886  df-un 3888  df-ss 3900  df-nul 4262  df-if 4455  df-sn 4556  df-pr 4558  df-op 4562  df-br 5073  df-dm 5628

This theorem is referenced by:  dmxpid  5872  rneq  5878  dmxpss  6122  dmsnopss  6165  dmsnsnsn  6171  f10d  6801  fndmin  6986  fninfp  7118  fndifnfp  7120  ovmpt3rabdm  7615  elxp4  7862  1stval  7933  fo1st  7951  f1stres  7955  bropopvvv  8029  bropfvvvv  8031  mpocurryd  8209  errn  8656  xpassen  8999  xpdom2  9000  oicl  9434  oif  9435  hartogslem1  9447  cantnfdm  9576  cantnfval  9580  cantnf0  9587  cantnfres  9589  cnfcomlem  9611  hsmexlem4  10342  hsmexlem5  10343  axdc3lem2  10364  ttukeylem3  10424  hashfun  14390  s1dmALT  14563  swrdval  14597  swrd0  14612  s2dmALT  14861  s4dom  14872  dmtrclfv  14971  relexpnndm  14994  relexpdmg  14995  relexpdmd  14997  relexpnnrn  14998  relexpfld  15002  relexpaddg  15006  shftdm  15024  rlim  15448  ramval  16970  isstruct2  17110  setsvalg  17127  setsdm  17131  prdsval  17409  homfeqbas  17653  invf  17726  dfiso2  17730  oppciso  17739  cicsym  17762  sscfn1  17775  sscfn2  17776  isssc  17778  rescval  17785  rescval2  17786  issubc  17793  issubc2  17794  cofuval  17840  resfval  17850  resfval2  17851  resf1st  17852  estrreslem2  18095  prfval  18156  lubdm  18306  glbdm  18319  joindm  18330  meetdm  18344  islat  18390  isclat  18457  oduclatb  18464  gsumvalx  18635  mndpsuppss  18724  cntzrcl  19293  f1omvdco2  19414  pmtrfrn  19424  symgsssg  19433  symgfisg  19434  symggen  19436  pmtrdifwrdellem3  19449  pmtrdifwrdel2lem1  19450  pmtrdifwrdel  19451  pmtrdifwrdel2  19452  psgnunilem1  19459  psgnunilem5  19460  psgnunilem2  19461  psgnunilem3  19462  psgneldm  19469  dmdprd  19966  dprdval  19971  dpjfval  20023  ablfaclem3  20055  cofipsgn  21568  elocv  21643  ishil  21693  dsmmval  21709  mpfrcl  22061  mamudm  22378  mavmuldm  22533  mavmul0g  22536  m1detdiag  22580  decpmatval0  22747  decpmatval  22748  pmatcollpw3lem  22766  iscnp2  23222  ptval  23553  ptcmplem2  24036  cnextfval  24045  tsmsval2  24113  ustbas2  24208  utopval  24215  tusval  24248  ucnval  24259  iscfilu  24270  psmetdmdm  24288  xmetdmdm  24318  blfvalps  24366  setsmstopn  24461  tmsval  24464  metuval  24532  tngtopn  24633  cfilfval  25249  caufval  25260  limcfval  25857  dvfval  25882  dvbsss  25887  perfdvf  25888  dvmptresicc  25901  dvn2bss  25915  dvnres  25916  dvcmul  25929  dvcmulf  25930  dvcj  25935  dvnfre  25937  dvexp  25938  dvmptres3  25941  dvmptcl  25944  dvmptadd  25945  dvmptmul  25946  dvmptres2  25947  dvmptcmul  25949  dvmptcj  25953  dvmptco  25957  rolle  25975  cmvth  25976  mvth  25977  dvlip  25978  dvlipcn  25979  dvlip2  25980  c1liplem1  25981  dveq0  25985  dv11cn  25986  dvle  25992  dvivthlem1  25993  dvivth  25995  dvne0  25996  lhop1lem  25998  lhop2  26000  lhop  26001  dvcnvrelem1  26002  dvcvx  26005  dvfsumle  26006  dvfsumge  26007  dvfsumabs  26008  dvmptrecl  26009  dvfsumlem2  26012  itgsubstlem  26033  taylfval  26342  tayl0  26345  dvtaylp  26353  dvntaylp  26354  dvntaylp0  26355  taylthlem1  26356  taylthlem2  26357  ulmdvlem1  26383  pserdv  26412  pige3ALT  26502  logtayl  26642  relogbf  26773  lgamgulmlem2  27011  nosupdm  27686  nosupbday  27687  nosupres  27689  nosupbnd1lem1  27690  nosupbnd1  27696  nosupbnd2  27698  noinfdm  27701  noinfbday  27702  noinfbnd1  27711  noinfbnd2  27713  perpln1  28796  isuhgr  29147  isushgr  29148  uhgreq12g  29152  isuhgrop  29157  uhgrun  29161  uhgrstrrepe  29165  isupgr  29171  upgrop  29181  isumgr  29182  upgr1e  29200  upgrun  29205  umgrun  29207  isuspgr  29239  isusgr  29240  isuspgrop  29248  isusgrop  29249  ausgrusgrb  29252  usgrstrrepe  29322  uspgr1e  29331  issubgr  29358  uhgrspansubgrlem  29377  usgrexi  29528  vtxdgfval  29554  vtxdeqd  29564  vtxdun  29568  1loopgrvd0  29591  1hevtxdg0  29592  1hevtxdg1  29593  umgr2v2e  29612  umgr2v2evd2  29614  ewlksfval  29688  wksfval  29696  wlkres  29755  wlkp1  29766  eupths  30288  eupthres  30303  trlsegvdeglem4  30311  trlsegvdeglem5  30312  grporndm  30599  hmoval  30899  gsumhashmul  33148  symgcom2  33165  symgcntz  33166  pmtrcnel2  33171  cycpmco2f1  33205  cycpmrn  33224  tocyccntz  33225  fxpval  33246  fxpgaval  33248  1arithidomlem2  33619  1arithidom  33620  minplyval  33889  smatrcl  33980  metidval  34074  pstmval  34079  prsssdm  34101  ordtrestNEW  34105  ofcfval  34282  ofcfval3  34286  brae  34425  braew  34426  faeval  34430  mbfmcst  34443  carsgval  34487  issibf  34517  sitmval  34533  0rrv  34635  dstrvprob  34656  fineqvac  35297  satfdm  35597  fmlafv  35608  fmla  35609  fmlasuc0  35612  satfdmfmla  35628  cnndvlem2  36844  bj-finsumval0  37645  cureq  37963  curf  37965  curunc  37969  sdclem2  38109  ismtyval  38167  isass  38213  isexid  38214  ismndo2  38241  exidreslem  38244  rngodm1dm2  38299  divrngcl  38324  isdrngo2  38325  cnvref4  38717  isopos  39672  isatl  39791  dibffval  41632  dibfval  41633  conrel2d  44108  iunrelexp0  44146  dmtrclfvRP  44174  rntrclfvRP  44175  neicvgbex  44556  dvsconst  44774  expgrowth  44779  fnlimfvre  46117  dvsinax  46356  dvcosax  46369  dvbdfbdioolem1  46371  itgsinexplem1  46397  itgcoscmulx  46412  dirkeritg  46545  dirkercncflem2  46547  fourierdlem60  46609  fourierdlem61  46610  fourierdlem74  46623  fourierdlem75  46624  fourierdlem80  46629  fourierdlem94  46643  fourierdlem103  46652  fourierdlem104  46653  fourierdlem113  46662  dmvon  47049  ovnovollem1  47099  smflimlem3  47216  smflimlem4  47217  smflim  47220  smflim2  47249  smfpimcc  47251  smflimmpt  47253  smfsuplem2  47255  smfsuplem3  47256  smfsup  47257  smfsupmpt  47258  smfinflem  47260  smfinf  47261  smfinfmpt  47262  smflimsuplem1  47263  smflimsuplem2  47264  smflimsuplem3  47265  smflimsuplem4  47266  smflimsuplem7  47269  smflimsup  47271  smflimsupmpt  47272  smfliminf  47274  smfliminfmpt  47275  dfateq12d  47589  isubgruhgr  48359  grimidvtxedg  48376  ushggricedg  48418  isubgrgrim  48420  stgrusgra  48450  gpgiedgdmel  48540  gpgusgra  48548  upwlksfval  48626  dmrnxp  49327  lubeldm2d  49448  glbeldm2d  49449  glbprlem  49455  isclatd  49473  isopropdlem  49530  dmdm  49543  infsubc2  49551  infsubc2d  49552  oppfvalg  49616  reldmprcof1  49871  reldmprcof2  49872  dfinito4  49991  reldmlan2  50107  reldmran2  50108  termolmd  50160