Theorem dmeqd 5897

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

This proof depends on syntax axioms:   → wi 4   = wceq 1570  dom cdm 5663

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2148  ax-9 2156  ax-ext 2737

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-sb 2100  df-clab 2744  df-cleq 2757  df-clel 2840  df-rab 3419  df-v 3459  df-dif 3909  df-un 3911  df-ss 3923  df-nul 4287  df-if 4490  df-sn 4592  df-pr 4594  df-op 4598  df-br 5112  df-dm 5673

This theorem is used by:  dmxpid  5922  rneq  5928  dmxpss  6171  dmsnopss  6217  dmsnsnsn  6223  f10d  6859  fndmin  7044  fninfp  7178  fndifnfp  7180  ovmpt3rabdm  7679  elxp4  7925  1stval  7994  fo1st  8012  f1stres  8016  bropopvvv  8091  bropfvvvv  8093  mpocurryd  8271  errn  8723  xpassen  9066  xpdom2  9067  oicl  9498  oif  9499  hartogslem1  9511  cantnfdm  9640  cantnfval  9644  cantnf0  9651  cantnfres  9653  cnfcomlem  9675  hsmexlem4  10428  hsmexlem5  10429  axdc3lem2  10450  ttukeylem3  10510  hashfun  14492  s1dmALT  14667  swrdval  14701  swrd0  14718  s2dmALT  14969  s4dom  14980  dmtrclfv  15079  relexpnndm  15102  relexpdmg  15103  relexpdmd  15105  relexpnnrn  15106  relexpfld  15110  relexpaddg  15114  shftdm  15132  rlim  15570  ramval  17090  isstruct2  17231  setsvalg  17248  setsdm  17252  prdsval  17530  homfeqbas  17774  invf  17847  dfiso2  17851  oppciso  17860  cicsym  17883  sscfn1  17896  sscfn2  17897  isssc  17899  rescval  17906  rescval2  17907  issubc  17914  issubc2  17915  cofuval  17961  resfval  17971  resfval2  17972  resf1st  17973  estrreslem2  18216  prfval  18277  lubdm  18427  glbdm  18440  joindm  18451  meetdm  18465  islat  18511  isclat  18578  oduclatb  18585  gsumvalx  18766  mndpsuppss  18860  cntzrcl  19441  f1omvdco2  19562  pmtrfrn  19572  symgsssg  19581  symgfisg  19582  symggen  19584  pmtrdifwrdellem3  19597  pmtrdifwrdel2lem1  19598  pmtrdifwrdel  19599  pmtrdifwrdel2  19600  psgnunilem1  19607  psgnunilem5  19608  psgnunilem2  19609  psgnunilem3  19610  psgneldm  19617  dmdprd  20114  dprdval  20119  dpjfval  20171  ablfaclem3  20203  cofipsgn  21793  elocv  21868  ishil  21918  dsmmval  21934  mpfrcl  22286  mamudm  22602  mavmuldm  22757  mavmul0g  22760  m1detdiag  22804  decpmatval0  22971  decpmatval  22972  pmatcollpw3lem  22990  iscnp2  23446  ptval  23778  ptcmplem2  24261  cnextfval  24270  tsmsval2  24338  ustbas2  24433  utopval  24440  tusval  24473  ucnval  24484  iscfilu  24495  psmetdmdm  24513  xmetdmdm  24543  blfvalps  24591  setsmstopn  24686  tmsval  24689  metuval  24757  tngtopn  24858  cfilfval  25474  caufval  25485  limcfval  26082  dvfval  26107  dvbsss  26112  perfdvf  26113  dvmptresicc  26126  dvn2bss  26140  dvnres  26141  dvcmul  26154  dvcmulf  26155  dvcj  26160  dvnfre  26162  dvexp  26163  dvmptres3  26166  dvmptcl  26169  dvmptadd  26170  dvmptmul  26171  dvmptres2  26172  dvmptcmul  26174  dvmptcj  26178  dvmptco  26182  rolle  26200  cmvth  26201  mvth  26202  dvlip  26203  dvlipcn  26204  dvlip2  26205  c1liplem1  26206  dveq0  26210  dv11cn  26211  dvle  26217  dvivthlem1  26218  dvivth  26220  dvne0  26221  lhop1lem  26223  lhop2  26225  lhop  26226  dvcnvrelem1  26227  dvcvx  26230  dvfsumle  26231  dvfsumge  26232  dvfsumabs  26233  dvmptrecl  26234  dvfsumlem2  26237  itgsubstlem  26258  taylfval  26573  tayl0  26576  dvtaylp  26584  dvntaylp  26585  dvntaylp0  26586  taylthlem1  26587  taylthlem2  26588  ulmdvlem1  26614  pserdv  26643  pige3ALT  26736  logtayl  26876  relogbf  27007  lgamgulmlem2  27245  nosupdm  27919  nosupbday  27920  nosupres  27922  nosupbnd1lem1  27923  nosupbnd1  27929  nosupbnd2  27931  noinfdm  27934  noinfbday  27935  noinfbnd1  27944  noinfbnd2  27946  perpln1  29041  isuhgr  29465  isushgr  29466  uhgreq12g  29470  isuhgrop  29475  uhgrun  29479  uhgrstrrepe  29483  isupgr  29489  upgrop  29499  isumgr  29500  upgr1e  29518  upgrun  29523  umgrun  29525  isuspgr  29560  isusgr  29561  isuspgrop  29569  isusgrop  29570  ausgrusgrb  29573  usgrstrrepe  29643  uspgr1e  29652  issubgr  29679  uhgrspansubgrlem  29698  usgrexi  29849  vtxdgfval  29875  vtxdeqd  29885  vtxdun  29889  1loopgrvd0  29912  1hevtxdg0  29913  1hevtxdg1  29914  umgr2v2e  29933  umgr2v2evd2  29935  ewlksfval  30009  wksfval  30017  wlkres  30076  wlkp1  30087  eupths  30622  eupthres  30637  trlsegvdeglem4  30645  trlsegvdeglem5  30646  grporndm  30933  hmoval  31233  gsumhashmul  33451  symgcom2  33468  symgcntz  33469  pmtrcnel2  33474  cycpmco2f1  33508  cycpmrn  33527  tocyccntz  33528  fxpval  33549  fxpgaval  33551  1arithidomlem2  33890  1arithidom  33891  minplyval  34159  smatrcl  34250  metidval  34344  pstmval  34349  prsssdm  34371  ordtrestNEW  34375  ofcfval  34552  ofcfval3  34556  brae  34696  braew  34697  faeval  34701  mbfmcst  34714  carsgval  34758  issibf  34788  sitmval  34804  0rrv  34906  dstrvprob  34927  fineqvac  35586  satfdm  35898  fmlafv  35909  fmla  35910  fmlasuc0  35913  satfdmfmla  35929  cnndvlem2  37184  bj-finsumval0  37986  cureq  38304  curf  38306  curunc  38310  sdclem2  38451  ismtyval  38509  isass  38555  isexid  38556  ismndo2  38583  exidreslem  38586  rngodm1dm2  38641  divrngcl  38666  isdrngo2  38667  cnvref4  39057  isopos  40012  isatl  40131  dibffval  41972  dibfval  41973  conrel2d  44448  iunrelexp0  44486  dmtrclfvRP  44514  rntrclfvRP  44515  neicvgbex  44896  dvsconst  45098  expgrowth  45103  fnlimfvre  46446  dvsinax  46685  dvcosax  46698  dvbdfbdioolem1  46700  itgsinexplem1  46726  itgcoscmulx  46741  dirkeritg  46874  dirkercncflem2  46876  fourierdlem60  46938  fourierdlem61  46939  fourierdlem74  46952  fourierdlem75  46953  fourierdlem80  46958  fourierdlem94  46972  fourierdlem103  46981  fourierdlem104  46982  fourierdlem113  46991  dmvon  47378  ovnovollem1  47428  smflimlem3  47545  smflimlem4  47546  smflim  47549  smflim2  47578  smfpimcc  47580  smflimmpt  47582  smfsuplem2  47584  smfsuplem3  47585  smfsup  47586  smfsupmpt  47587  smfinflem  47589  smfinf  47590  smfinfmpt  47591  smflimsuplem1  47592  smflimsuplem2  47593  smflimsuplem3  47594  smflimsuplem4  47595  smflimsuplem7  47598  smflimsup  47600  smflimsupmpt  47601  smfliminf  47603  smfliminfmpt  47604  dfateq12d  47921  isubgruhgr  48691  grimidvtxedg  48708  ushggricedg  48750  isubgrgrim  48752  stgrusgra  48782  gpgiedgdmel  48872  gpgusgra  48880  upwlksfval  48958  dmrnxp  49672  lubeldm2d  49793  glbeldm2d  49794  glbprlem  49800  isclatd  49818  isopropdlem  49875  dmdm  49888  infsubc2  49896  infsubc2d  49897  oppfvalg  49961  reldmprcof1  50216  reldmprcof2  50217  dfinito4  50336  reldmlan2  50452  reldmran2  50453  termolmd  50505