Theorem dmeqd 5906

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

Syntax hints:   → wi 4   = wceq 1542  dom cdm 5677

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2704

This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1783  df-sb 2069  df-clab 2711  df-cleq 2725  df-clel 2811  df-rab 3434  df-v 3477  df-dif 3952  df-un 3954  df-in 3956  df-ss 3966  df-nul 4324  df-if 4530  df-sn 4630  df-pr 4632  df-op 4636  df-br 5150  df-dm 5687

This theorem is referenced by:  dmxpid  5930  rneq  5936  dmxpss  6171  dmsnopss  6214  dmsnsnsn  6220  f10d  6868  fndmin  7047  fninfp  7172  fndifnfp  7174  ovmpt3rabdm  7665  elxp4  7913  1stval  7977  fo1st  7995  f1stres  7999  bropopvvv  8076  bropfvvvv  8078  mpocurryd  8254  errn  8725  xpassen  9066  xpdom2  9067  oicl  9524  oif  9525  hartogslem1  9537  cantnfdm  9659  cantnfval  9663  cantnf0  9670  cantnfres  9672  cnfcomlem  9694  hsmexlem4  10424  hsmexlem5  10425  axdc3lem2  10446  ttukeylem3  10506  hashfun  14397  s1dmALT  14559  swrdval  14593  swrd0  14608  s2dmALT  14859  s4dom  14870  dmtrclfv  14965  relexpnndm  14988  relexpdmg  14989  relexpdmd  14991  relexpnnrn  14992  relexpfld  14996  relexpaddg  15000  shftdm  15018  rlim  15439  ramval  16941  isstruct2  17082  setsvalg  17099  setsdm  17103  prdsval  17401  homfeqbas  17640  invf  17715  dfiso2  17719  oppciso  17728  cicsym  17751  sscfn1  17764  sscfn2  17765  isssc  17767  rescval  17774  rescval2  17775  issubc  17785  issubc2  17786  cofuval  17832  resfval  17842  resfval2  17843  resf1st  17844  estrreslem2  18090  prfval  18151  lubdm  18304  glbdm  18317  joindm  18328  meetdm  18342  islat  18386  isclat  18453  oduclatb  18460  gsumvalx  18595  cntzrcl  19191  f1omvdco2  19316  pmtrfrn  19326  symgsssg  19335  symgfisg  19336  symggen  19338  pmtrdifwrdellem3  19351  pmtrdifwrdel2lem1  19352  pmtrdifwrdel  19353  pmtrdifwrdel2  19354  psgnunilem1  19361  psgnunilem5  19362  psgnunilem2  19363  psgnunilem3  19364  psgneldm  19371  dmdprd  19868  dprdval  19873  dpjfval  19925  ablfaclem3  19957  cofipsgn  21146  elocv  21221  ishil  21273  dsmmval  21289  mpfrcl  21648  mamudm  21890  mavmuldm  22052  mavmul0g  22055  m1detdiag  22099  decpmatval0  22266  decpmatval  22267  pmatcollpw3lem  22285  iscnp2  22743  ptval  23074  ptcmplem2  23557  cnextfval  23566  tsmsval2  23634  ustbas2  23730  utopval  23737  tusval  23770  ucnval  23782  iscfilu  23793  psmetdmdm  23811  xmetdmdm  23841  blfvalps  23889  setsmstopn  23986  tmsval  23989  metuval  24058  tngtopn  24167  cfilfval  24781  caufval  24792  limcfval  25389  dvfval  25414  dvbsss  25419  perfdvf  25420  dvmptresicc  25433  dvn2bss  25447  dvnres  25448  dvcmul  25461  dvcmulf  25462  dvcj  25467  dvnfre  25469  dvexp  25470  dvmptres3  25473  dvmptcl  25476  dvmptadd  25477  dvmptmul  25478  dvmptres2  25479  dvmptcmul  25481  dvmptcj  25485  dvmptco  25489  rolle  25507  cmvth  25508  mvth  25509  dvlip  25510  dvlipcn  25511  dvlip2  25512  c1liplem1  25513  dveq0  25517  dv11cn  25518  dvle  25524  dvivthlem1  25525  dvivth  25527  dvne0  25528  lhop1lem  25530  lhop2  25532  lhop  25533  dvcnvrelem1  25534  dvcvx  25537  dvfsumle  25538  dvfsumge  25539  dvfsumabs  25540  dvmptrecl  25541  dvfsumlem2  25544  itgsubstlem  25565  taylfval  25871  tayl0  25874  dvtaylp  25882  dvntaylp  25883  dvntaylp0  25884  taylthlem1  25885  taylthlem2  25886  ulmdvlem1  25912  pserdv  25941  pige3ALT  26029  logtayl  26168  relogbf  26296  lgamgulmlem2  26534  nosupdm  27207  nosupbday  27208  nosupres  27210  nosupbnd1lem1  27211  nosupbnd1  27217  nosupbnd2  27219  noinfdm  27222  noinfbday  27223  noinfbnd1  27232  noinfbnd2  27234  perpln1  27961  isuhgr  28320  isushgr  28321  uhgreq12g  28325  isuhgrop  28330  uhgrun  28334  uhgrstrrepe  28338  isupgr  28344  upgrop  28354  isumgr  28355  upgr1e  28373  upgrun  28378  umgrun  28380  isuspgr  28412  isusgr  28413  isuspgrop  28421  isusgrop  28422  ausgrusgrb  28425  usgrstrrepe  28492  uspgr1e  28501  usgrexmpl  28520  issubgr  28528  uhgrspansubgrlem  28547  usgrexi  28698  vtxdgfval  28724  vtxdeqd  28734  vtxdun  28738  1loopgrvd0  28761  1hevtxdg0  28762  1hevtxdg1  28763  umgr2v2e  28782  umgr2v2evd2  28784  ewlksfval  28858  wksfval  28866  wlkres  28927  wlkp1  28938  eupths  29453  eupthres  29468  trlsegvdeglem4  29476  trlsegvdeglem5  29477  grporndm  29763  hmoval  30063  gsumhashmul  32208  symgcom2  32245  symgcntz  32246  pmtrcnel2  32251  cycpmco2f1  32283  cycpmrn  32302  tocyccntz  32303  minplyval  32766  smatrcl  32776  metidval  32870  pstmval  32875  prsssdm  32897  ordtrestNEW  32901  ofcfval  33096  ofcfval3  33100  brae  33239  braew  33240  faeval  33244  mbfmcst  33258  carsgval  33302  issibf  33332  sitmval  33348  0rrv  33450  dstrvprob  33470  fineqvac  34097  satfdm  34360  fmlafv  34371  fmla  34372  fmlasuc0  34375  satfdmfmla  34391  gg-cmvth  35181  gg-dvfsumle  35182  gg-dvfsumlem2  35183  cnndvlem2  35414  bj-finsumval0  36166  cureq  36464  curf  36466  curunc  36470  sdclem2  36610  ismtyval  36668  isass  36714  isexid  36715  ismndo2  36742  exidreslem  36745  rngodm1dm2  36800  divrngcl  36825  isdrngo2  36826  cnvref4  37219  isopos  38050  isatl  38169  dibffval  40011  dibfval  40012  conrel2d  42415  iunrelexp0  42453  dmtrclfvRP  42481  rntrclfvRP  42482  neicvgbex  42863  dvsconst  43089  expgrowth  43094  fnlimfvre  44390  dvsinax  44629  dvcosax  44642  dvbdfbdioolem1  44644  itgsinexplem1  44670  itgcoscmulx  44685  dirkeritg  44818  dirkercncflem2  44820  fourierdlem60  44882  fourierdlem61  44883  fourierdlem74  44896  fourierdlem75  44897  fourierdlem80  44902  fourierdlem94  44916  fourierdlem103  44925  fourierdlem104  44926  fourierdlem113  44935  dmvon  45322  ovnovollem1  45372  smflimlem3  45489  smflimlem4  45490  smflim  45493  smflim2  45522  smfpimcc  45524  smflimmpt  45526  smfsuplem2  45528  smfsuplem3  45529  smfsup  45530  smfsupmpt  45531  smfinflem  45533  smfinf  45534  smfinfmpt  45535  smflimsuplem1  45536  smflimsuplem2  45537  smflimsuplem3  45538  smflimsuplem4  45539  smflimsuplem7  45542  smflimsup  45544  smflimsupmpt  45545  smfliminf  45547  smfliminfmpt  45548  dfateq12d  45834  isomgr  46491  isomgreqve  46493  ushrisomgr  46509  upwlksfval  46513  mndpsuppss  47047  lubeldm2d  47591  glbeldm2d  47592  glbprlem  47598  isclatd  47608