Theorem dmeqd 5899

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

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

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 1945  ax-6 2002  ax-7 2043  ax-8 2149  ax-9 2157  ax-ext 2735

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 2102  df-clab 2742  df-cleq 2755  df-clel 2839  df-rab 3417  df-v 3456  df-ss 3901  df-dif 4050  df-un 4154  df-nul 4282  df-if 4486  df-sn 4589  df-pr 4591  df-op 4841  df-br 5109  df-dm 5668

This theorem is used by:  dmxpid  5924  rneq  5930  dmxpss  6181  dmsnopss  6234  dmsnsnsn  6240  f10d  6890  fndmin  7075  fninfp  7210  fndifnfp  7212  ovmpt3rabdm  7712  elxp4  7968  1stval  8037  fo1st  8055  f1stres  8059  bropopvvv  8136  bropfvvvv  8138  mpocurryd  8324  errn  8778  cureq  8927  curf  8928  xpassen  9128  xpdom2  9129  oicl  9560  oif  9561  hartogslem1  9573  cantnfdm  9702  cantnfval  9706  cantnf0  9713  cantnfres  9715  cnfcomlem  9737  hsmexlem4  10546  hsmexlem5  10547  axdc3lem2  10568  ttukeylem3  10628  hashfun  14623  s1dmALT  14799  swrdval  14833  swrd0  14850  s2dmALT  15102  s4dom  15113  dmtrclfv  15214  relexpnndm  15237  relexpdmg  15238  relexpdmd  15240  relexpnnrn  15241  relexpfld  15245  relexpaddg  15249  shftdm  15267  rlim  15706  ramval  17230  isstruct2  17371  setsvalg  17388  setsdm  17392  prdsval  17676  homfeqbas  17920  invf  17993  dfiso2  17997  oppciso  18006  cicsym  18029  sscfn1  18042  sscfn2  18043  isssc  18045  rescval  18052  rescval2  18053  issubc  18060  issubc2  18061  cofuval  18107  resfval  18117  resfval2  18118  resf1st  18119  estrreslem2  18362  prfval  18423  lubdm  18573  glbdm  18586  joindm  18597  meetdm  18611  islat  18657  isclat  18724  oduclatb  18731  gsumvalx  18915  mndpsuppss  19009  cntzrcl  19592  f1omvdco2  19713  pmtrfrn  19723  symgsssg  19732  symgfisg  19733  symggen  19735  pmtrdifwrdellem3  19748  pmtrdifwrdel2lem1  19749  pmtrdifwrdel  19750  pmtrdifwrdel2  19751  psgnunilem1  19758  psgnunilem5  19759  psgnunilem2  19760  psgnunilem3  19761  psgneldm  19768  dmdprd  20265  dprdval  20270  dpjfval  20322  ablfaclem3  20354  cofipsgn  21954  elocv  22029  ishil  22079  dsmmval  22095  mpfrcl  22449  mamudm  22765  mavmuldm  22920  mavmul0g  22923  m1detdiag  22967  decpmatval0  23137  decpmatval  23138  pmatcollpw3lem  23156  iscnp2  23612  ptval  23944  ptcmplem2  24427  cnextfval  24436  tsmsval2  24504  ustbas2  24599  utopval  24606  tusval  24639  ucnval  24650  iscfilu  24661  psmetdmdm  24679  xmetdmdm  24709  blfvalps  24757  setsmstopn  24852  tmsval  24855  metuval  24923  tngtopn  25024  cfilfval  25640  caufval  25651  limcfval  26247  dvfval  26272  dvbsss  26277  perfdvf  26278  dvmptresicc  26291  dvn2bss  26305  dvnres  26306  dvcmul  26319  dvcmulf  26320  dvcj  26325  dvnfre  26327  dvexp  26328  dvmptres3  26331  dvmptcl  26334  dvmptadd  26335  dvmptmul  26336  dvmptres2  26337  dvmptcmul  26339  dvmptcj  26343  dvmptco  26347  rolle  26365  cmvth  26366  mvth  26367  dvlip  26368  dvlipcn  26369  dvlip2  26370  c1liplem1  26371  dveq0  26375  dv11cn  26376  dvle  26382  dvivthlem1  26383  dvivth  26385  dvne0  26386  lhop1lem  26388  lhop2  26390  lhop  26391  dvcnvrelem1  26392  dvcvx  26395  dvfsumle  26396  dvfsumge  26397  dvfsumabs  26398  dvmptrecl  26399  dvfsumlem2  26402  itgsubstlem  26423  taylfval  26743  tayl0  26746  dvtaylp  26754  dvntaylp  26755  dvntaylp0  26756  taylthlem1  26757  taylthlem2  26758  ulmdvlem1  26784  pserdv  26813  pige3ALT  26905  logtayl  27045  relogbf  27176  lgamgulmlem2  27414  nosupdm  28118  nosupbday  28119  nosupres  28121  nosupbnd1lem1  28122  nosupbnd1  28128  nosupbnd2  28130  noinfdm  28133  noinfbday  28134  noinfbnd1  28143  noinfbnd2  28145  perpln1  29242  isuhgr  29695  isushgr  29696  uhgreq12g  29700  isuhgrop  29705  uhgrun  29709  uhgrstrrepe  29713  isupgr  29719  upgrop  29729  isumgr  29730  upgr1e  29748  upgrun  29753  umgrun  29755  isuspgr  29790  isusgr  29791  isuspgrop  29799  isusgrop  29800  ausgrusgrb  29803  usgrstrrepe  29873  uspgr1e  29882  issubgr  29909  uhgrspansubgrlem  29928  usgrexi  30079  vtxdgfval  30105  vtxdeqd  30115  vtxdun  30119  1loopgrvd0  30142  1hevtxdg0  30143  1hevtxdg1  30144  umgr2v2e  30163  umgr2v2evd2  30165  ewlksfval  30239  wksfval  30247  wlkres  30306  wlkp1  30317  eupths  30858  eupthres  30873  trlsegvdeglem4  30881  trlsegvdeglem5  30882  grporndm  31169  hmoval  31469  gsumhashmul  33727  symgcom2  33744  symgcntz  33745  pmtrcnel2  33750  cycpmco2f1  33784  cycpmrn  33803  tocyccntz  33804  fxpval  33825  fxpgaval  33827  1arithidomlem2  34172  1arithidom  34173  minplyval  34448  smatrcl  34539  metidval  34633  pstmval  34638  prsssdm  34660  ordtrestNEW  34664  ofcfval  34841  ofcfval3  34845  brae  34985  braew  34986  faeval  34990  mbfmcst  35002  carsgval  35046  issibf  35076  sitmval  35092  0rrv  35194  dstrvprob  35215  fineqvac  35925  satfdm  36342  fmlafv  36353  fmla  36354  fmlasuc0  36357  satfdmfmla  36373  cnndvlem2  37619  bj-finsumval0  38474  curunc  38793  sdclem2  38942  ismtyval  39000  isass  39046  isexid  39047  ismndo2  39074  exidreslem  39077  rngodm1dm2  39132  divrngcl  39157  isdrngo2  39158  cnvref4  39548  isopos  40503  isatl  40622  dibffval  42463  dibfval  42464  conrel2d  44925  iunrelexp0  44963  dmtrclfvRP  44991  rntrclfvRP  44992  neicvgbex  45373  dvsconst  45575  expgrowth  45580  fnlimfvre  46957  dvsinax  47196  dvcosax  47209  dvbdfbdioolem1  47211  itgsinexplem1  47237  itgcoscmulx  47252  dirkeritg  47385  dirkercncflem2  47387  fourierdlem60  47449  fourierdlem61  47450  fourierdlem74  47463  fourierdlem75  47464  fourierdlem80  47469  fourierdlem94  47483  fourierdlem103  47492  fourierdlem104  47493  fourierdlem113  47502  dmvon  47889  ovnovollem1  47939  smflimlem3  48056  smflimlem4  48057  smflim  48060  smflim2  48089  smfpimcc  48091  smflimmpt  48093  smfsuplem2  48095  smfsuplem3  48096  smfsup  48097  smfsupmpt  48098  smfinflem  48100  smfinf  48101  smfinfmpt  48102  smflimsuplem1  48103  smflimsuplem2  48104  smflimsuplem3  48105  smflimsuplem4  48106  smflimsuplem7  48109  smflimsup  48111  smflimsupmpt  48112  smfliminf  48114  smfliminfmpt  48115  tmachlem-agreefin  48231  dfateq12d  48469  isubgruhgr  49239  grimidvtxedg  49256  ushggricedg  49298  isubgrgrim  49300  stgrusgra  49330  gpgiedgdmel  49420  gpgusgra  49428  upwlksfval  49506  dmrnxp  50279  lubeldm2d  50403  glbeldm2d  50404  glbprlem  50410  isclatd  50428  isopropdlem  50485  dmdm  50498  infsubc2  50506  infsubc2d  50507  oppfvalg  50573  reldmprcof1  50847  reldmprcof2  50848  dfinito4  50967  termccofix  51002  reldmlan2  51131  reldmran2  51132  termolmd  51184