Theorem dmeqd 5887

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

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

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 2147  ax-9 2155  ax-ext 2733

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 2740  df-cleq 2753  df-clel 2836  df-rab 3414  df-v 3453  df-dif 3902  df-un 3904  df-ss 3916  df-nul 4280  df-if 4483  df-sn 4585  df-pr 4587  df-op 4591  df-br 5104  df-dm 5661

This theorem is used by:  dmxpid  5912  rneq  5918  dmxpss  6163  dmsnopss  6214  dmsnsnsn  6220  f10d  6857  fndmin  7042  fninfp  7177  fndifnfp  7179  ovmpt3rabdm  7678  elxp4  7932  1stval  8001  fo1st  8019  f1stres  8023  bropopvvv  8099  bropfvvvv  8101  mpocurryd  8279  errn  8733  cureq  8882  curf  8883  xpassen  9083  xpdom2  9084  oicl  9516  oif  9517  hartogslem1  9529  cantnfdm  9658  cantnfval  9662  cantnf0  9669  cantnfres  9671  cnfcomlem  9693  hsmexlem4  10500  hsmexlem5  10501  axdc3lem2  10522  ttukeylem3  10582  hashfun  14575  s1dmALT  14750  swrdval  14784  swrd0  14801  s2dmALT  15052  s4dom  15063  dmtrclfv  15164  relexpnndm  15187  relexpdmg  15188  relexpdmd  15190  relexpnnrn  15191  relexpfld  15195  relexpaddg  15199  shftdm  15217  rlim  15655  ramval  17179  isstruct2  17320  setsvalg  17337  setsdm  17341  prdsval  17619  homfeqbas  17863  invf  17936  dfiso2  17940  oppciso  17949  cicsym  17972  sscfn1  17985  sscfn2  17986  isssc  17988  rescval  17995  rescval2  17996  issubc  18003  issubc2  18004  cofuval  18050  resfval  18060  resfval2  18061  resf1st  18062  estrreslem2  18305  prfval  18366  lubdm  18516  glbdm  18529  joindm  18540  meetdm  18554  islat  18600  isclat  18667  oduclatb  18674  gsumvalx  18858  mndpsuppss  18952  cntzrcl  19534  f1omvdco2  19655  pmtrfrn  19665  symgsssg  19674  symgfisg  19675  symggen  19677  pmtrdifwrdellem3  19690  pmtrdifwrdel2lem1  19691  pmtrdifwrdel  19692  pmtrdifwrdel2  19693  psgnunilem1  19700  psgnunilem5  19701  psgnunilem2  19702  psgnunilem3  19703  psgneldm  19710  dmdprd  20207  dprdval  20212  dpjfval  20264  ablfaclem3  20296  cofipsgn  21892  elocv  21967  ishil  22017  dsmmval  22033  mpfrcl  22387  mamudm  22703  mavmuldm  22858  mavmul0g  22861  m1detdiag  22905  decpmatval0  23075  decpmatval  23076  pmatcollpw3lem  23094  iscnp2  23550  ptval  23882  ptcmplem2  24365  cnextfval  24374  tsmsval2  24442  ustbas2  24537  utopval  24544  tusval  24577  ucnval  24588  iscfilu  24599  psmetdmdm  24617  xmetdmdm  24647  blfvalps  24695  setsmstopn  24790  tmsval  24793  metuval  24861  tngtopn  24962  cfilfval  25578  caufval  25589  limcfval  26185  dvfval  26210  dvbsss  26215  perfdvf  26216  dvmptresicc  26229  dvn2bss  26243  dvnres  26244  dvcmul  26257  dvcmulf  26258  dvcj  26263  dvnfre  26265  dvexp  26266  dvmptres3  26269  dvmptcl  26272  dvmptadd  26273  dvmptmul  26274  dvmptres2  26275  dvmptcmul  26277  dvmptcj  26281  dvmptco  26285  rolle  26303  cmvth  26304  mvth  26305  dvlip  26306  dvlipcn  26307  dvlip2  26308  c1liplem1  26309  dveq0  26313  dv11cn  26314  dvle  26320  dvivthlem1  26321  dvivth  26323  dvne0  26324  lhop1lem  26326  lhop2  26328  lhop  26329  dvcnvrelem1  26330  dvcvx  26333  dvfsumle  26334  dvfsumge  26335  dvfsumabs  26336  dvmptrecl  26337  dvfsumlem2  26340  itgsubstlem  26361  taylfval  26679  tayl0  26682  dvtaylp  26690  dvntaylp  26691  dvntaylp0  26692  taylthlem1  26693  taylthlem2  26694  ulmdvlem1  26720  pserdv  26749  pige3ALT  26841  logtayl  26981  relogbf  27112  lgamgulmlem2  27350  nosupdm  28054  nosupbday  28055  nosupres  28057  nosupbnd1lem1  28058  nosupbnd1  28064  nosupbnd2  28066  noinfdm  28069  noinfbday  28070  noinfbnd1  28079  noinfbnd2  28081  perpln1  29178  isuhgr  29631  isushgr  29632  uhgreq12g  29636  isuhgrop  29641  uhgrun  29645  uhgrstrrepe  29649  isupgr  29655  upgrop  29665  isumgr  29666  upgr1e  29684  upgrun  29689  umgrun  29691  isuspgr  29726  isusgr  29727  isuspgrop  29735  isusgrop  29736  ausgrusgrb  29739  usgrstrrepe  29809  uspgr1e  29818  issubgr  29845  uhgrspansubgrlem  29864  usgrexi  30015  vtxdgfval  30041  vtxdeqd  30051  vtxdun  30055  1loopgrvd0  30078  1hevtxdg0  30079  1hevtxdg1  30080  umgr2v2e  30099  umgr2v2evd2  30101  ewlksfval  30175  wksfval  30183  wlkres  30242  wlkp1  30253  eupths  30794  eupthres  30809  trlsegvdeglem4  30817  trlsegvdeglem5  30818  grporndm  31105  hmoval  31405  gsumhashmul  33621  symgcom2  33638  symgcntz  33639  pmtrcnel2  33644  cycpmco2f1  33678  cycpmrn  33697  tocyccntz  33698  fxpval  33719  fxpgaval  33721  1arithidomlem2  34061  1arithidom  34062  minplyval  34330  smatrcl  34421  metidval  34515  pstmval  34520  prsssdm  34542  ordtrestNEW  34546  ofcfval  34723  ofcfval3  34727  brae  34867  braew  34868  faeval  34872  mbfmcst  34884  carsgval  34928  issibf  34958  sitmval  34974  0rrv  35076  dstrvprob  35097  fineqvac  35767  satfdm  36113  fmlafv  36124  fmla  36125  fmlasuc0  36128  satfdmfmla  36144  cnndvlem2  37384  bj-finsumval0  38186  curunc  38505  sdclem2  38656  ismtyval  38714  isass  38760  isexid  38761  ismndo2  38788  exidreslem  38791  rngodm1dm2  38846  divrngcl  38871  isdrngo2  38872  cnvref4  39262  isopos  40217  isatl  40336  dibffval  42177  dibfval  42178  conrel2d  44649  iunrelexp0  44687  dmtrclfvRP  44715  rntrclfvRP  44716  neicvgbex  45097  dvsconst  45299  expgrowth  45304  fnlimfvre  46653  dvsinax  46892  dvcosax  46905  dvbdfbdioolem1  46907  itgsinexplem1  46933  itgcoscmulx  46948  dirkeritg  47081  dirkercncflem2  47083  fourierdlem60  47145  fourierdlem61  47146  fourierdlem74  47159  fourierdlem75  47160  fourierdlem80  47165  fourierdlem94  47179  fourierdlem103  47188  fourierdlem104  47189  fourierdlem113  47198  dmvon  47585  ovnovollem1  47635  smflimlem3  47752  smflimlem4  47753  smflim  47756  smflim2  47785  smfpimcc  47787  smflimmpt  47789  smfsuplem2  47791  smfsuplem3  47792  smfsup  47793  smfsupmpt  47794  smfinflem  47796  smfinf  47797  smfinfmpt  47798  smflimsuplem1  47799  smflimsuplem2  47800  smflimsuplem3  47801  smflimsuplem4  47802  smflimsuplem7  47805  smflimsup  47807  smflimsupmpt  47808  smfliminf  47810  smfliminfmpt  47811  tmachlem-agreefin  47927  dfateq12d  48165  isubgruhgr  48935  grimidvtxedg  48952  ushggricedg  48994  isubgrgrim  48996  stgrusgra  49026  gpgiedgdmel  49116  gpgusgra  49124  upwlksfval  49202  dmrnxp  49916  lubeldm2d  50035  glbeldm2d  50036  glbprlem  50042  isclatd  50060  isopropdlem  50117  dmdm  50130  infsubc2  50138  infsubc2d  50139  oppfvalg  50203  reldmprcof1  50458  reldmprcof2  50459  dfinito4  50578  reldmlan2  50694  reldmran2  50695  termolmd  50747