Theorem dmeqd 5860

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

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-sb 2069  df-clab 2715  df-cleq 2728  df-clel 2811  df-rab 3390  df-v 3431  df-dif 3892  df-un 3894  df-ss 3906  df-nul 4274  df-if 4467  df-sn 4568  df-pr 4570  df-op 4574  df-br 5086  df-dm 5641

This theorem is referenced by:  dmxpid  5885  rneq  5891  dmxpss  6135  dmsnopss  6178  dmsnsnsn  6184  f10d  6814  fndmin  6997  fninfp  7129  fndifnfp  7131  ovmpt3rabdm  7626  elxp4  7873  1stval  7944  fo1st  7962  f1stres  7966  bropopvvv  8040  bropfvvvv  8042  mpocurryd  8219  errn  8666  xpassen  9009  xpdom2  9010  oicl  9444  oif  9445  hartogslem1  9457  cantnfdm  9585  cantnfval  9589  cantnf0  9596  cantnfres  9598  cnfcomlem  9620  hsmexlem4  10351  hsmexlem5  10352  axdc3lem2  10373  ttukeylem3  10433  hashfun  14399  s1dmALT  14572  swrdval  14606  swrd0  14621  s2dmALT  14870  s4dom  14881  dmtrclfv  14980  relexpnndm  15003  relexpdmg  15004  relexpdmd  15006  relexpnnrn  15007  relexpfld  15011  relexpaddg  15015  shftdm  15033  rlim  15457  ramval  16979  isstruct2  17119  setsvalg  17136  setsdm  17140  prdsval  17418  homfeqbas  17662  invf  17735  dfiso2  17739  oppciso  17748  cicsym  17771  sscfn1  17784  sscfn2  17785  isssc  17787  rescval  17794  rescval2  17795  issubc  17802  issubc2  17803  cofuval  17849  resfval  17859  resfval2  17860  resf1st  17861  estrreslem2  18104  prfval  18165  lubdm  18315  glbdm  18328  joindm  18339  meetdm  18353  islat  18399  isclat  18466  oduclatb  18473  gsumvalx  18644  mndpsuppss  18733  cntzrcl  19302  f1omvdco2  19423  pmtrfrn  19433  symgsssg  19442  symgfisg  19443  symggen  19445  pmtrdifwrdellem3  19458  pmtrdifwrdel2lem1  19459  pmtrdifwrdel  19460  pmtrdifwrdel2  19461  psgnunilem1  19468  psgnunilem5  19469  psgnunilem2  19470  psgnunilem3  19471  psgneldm  19478  dmdprd  19975  dprdval  19980  dpjfval  20032  ablfaclem3  20064  cofipsgn  21573  elocv  21648  ishil  21698  dsmmval  21714  mpfrcl  22063  mamudm  22360  mavmuldm  22515  mavmul0g  22518  m1detdiag  22562  decpmatval0  22729  decpmatval  22730  pmatcollpw3lem  22748  iscnp2  23204  ptval  23535  ptcmplem2  24018  cnextfval  24027  tsmsval2  24095  ustbas2  24190  utopval  24197  tusval  24230  ucnval  24241  iscfilu  24252  psmetdmdm  24270  xmetdmdm  24300  blfvalps  24348  setsmstopn  24443  tmsval  24446  metuval  24514  tngtopn  24615  cfilfval  25231  caufval  25242  limcfval  25839  dvfval  25864  dvbsss  25869  perfdvf  25870  dvmptresicc  25883  dvn2bss  25897  dvnres  25898  dvcmul  25911  dvcmulf  25912  dvcj  25917  dvnfre  25919  dvexp  25920  dvmptres3  25923  dvmptcl  25926  dvmptadd  25927  dvmptmul  25928  dvmptres2  25929  dvmptcmul  25931  dvmptcj  25935  dvmptco  25939  rolle  25957  cmvth  25958  mvth  25959  dvlip  25960  dvlipcn  25961  dvlip2  25962  c1liplem1  25963  dveq0  25967  dv11cn  25968  dvle  25974  dvivthlem1  25975  dvivth  25977  dvne0  25978  lhop1lem  25980  lhop2  25982  lhop  25983  dvcnvrelem1  25984  dvcvx  25987  dvfsumle  25988  dvfsumge  25989  dvfsumabs  25990  dvmptrecl  25991  dvfsumlem2  25994  itgsubstlem  26015  taylfval  26324  tayl0  26327  dvtaylp  26335  dvntaylp  26336  dvntaylp0  26337  taylthlem1  26338  taylthlem2  26339  ulmdvlem1  26365  pserdv  26394  pige3ALT  26484  logtayl  26624  relogbf  26755  lgamgulmlem2  26993  nosupdm  27668  nosupbday  27669  nosupres  27671  nosupbnd1lem1  27672  nosupbnd1  27678  nosupbnd2  27680  noinfdm  27683  noinfbday  27684  noinfbnd1  27693  noinfbnd2  27695  perpln1  28778  isuhgr  29129  isushgr  29130  uhgreq12g  29134  isuhgrop  29139  uhgrun  29143  uhgrstrrepe  29147  isupgr  29153  upgrop  29163  isumgr  29164  upgr1e  29182  upgrun  29187  umgrun  29189  isuspgr  29221  isusgr  29222  isuspgrop  29230  isusgrop  29231  ausgrusgrb  29234  usgrstrrepe  29304  uspgr1e  29313  issubgr  29340  uhgrspansubgrlem  29359  usgrexi  29510  vtxdgfval  29536  vtxdeqd  29546  vtxdun  29550  1loopgrvd0  29573  1hevtxdg0  29574  1hevtxdg1  29575  umgr2v2e  29594  umgr2v2evd2  29596  ewlksfval  29670  wksfval  29678  wlkres  29737  wlkp1  29748  eupths  30270  eupthres  30285  trlsegvdeglem4  30293  trlsegvdeglem5  30294  grporndm  30581  hmoval  30881  gsumhashmul  33128  symgcom2  33145  symgcntz  33146  pmtrcnel2  33151  cycpmco2f1  33185  cycpmrn  33204  tocyccntz  33205  fxpval  33226  fxpgaval  33228  1arithidomlem2  33596  1arithidom  33597  minplyval  33849  smatrcl  33940  metidval  34034  pstmval  34039  prsssdm  34061  ordtrestNEW  34065  ofcfval  34242  ofcfval3  34246  brae  34385  braew  34386  faeval  34390  mbfmcst  34403  carsgval  34447  issibf  34477  sitmval  34493  0rrv  34595  dstrvprob  34616  fineqvac  35260  satfdm  35551  fmlafv  35562  fmla  35563  fmlasuc0  35566  satfdmfmla  35582  cnndvlem2  36798  bj-finsumval0  37599  cureq  37917  curf  37919  curunc  37923  sdclem2  38063  ismtyval  38121  isass  38167  isexid  38168  ismndo2  38195  exidreslem  38198  rngodm1dm2  38253  divrngcl  38278  isdrngo2  38279  cnvref4  38671  isopos  39626  isatl  39745  dibffval  41586  dibfval  41587  conrel2d  44091  iunrelexp0  44129  dmtrclfvRP  44157  rntrclfvRP  44158  neicvgbex  44539  dvsconst  44757  expgrowth  44762  fnlimfvre  46102  dvsinax  46341  dvcosax  46354  dvbdfbdioolem1  46356  itgsinexplem1  46382  itgcoscmulx  46397  dirkeritg  46530  dirkercncflem2  46532  fourierdlem60  46594  fourierdlem61  46595  fourierdlem74  46608  fourierdlem75  46609  fourierdlem80  46614  fourierdlem94  46628  fourierdlem103  46637  fourierdlem104  46638  fourierdlem113  46647  dmvon  47034  ovnovollem1  47084  smflimlem3  47201  smflimlem4  47202  smflim  47205  smflim2  47234  smfpimcc  47236  smflimmpt  47238  smfsuplem2  47240  smfsuplem3  47241  smfsup  47242  smfsupmpt  47243  smfinflem  47245  smfinf  47246  smfinfmpt  47247  smflimsuplem1  47248  smflimsuplem2  47249  smflimsuplem3  47250  smflimsuplem4  47251  smflimsuplem7  47254  smflimsup  47256  smflimsupmpt  47257  smfliminf  47259  smfliminfmpt  47260  dfateq12d  47574  isubgruhgr  48344  grimidvtxedg  48361  ushggricedg  48403  isubgrgrim  48405  stgrusgra  48435  gpgiedgdmel  48525  gpgusgra  48533  upwlksfval  48611  dmrnxp  49312  lubeldm2d  49433  glbeldm2d  49434  glbprlem  49440  isclatd  49458  isopropdlem  49515  dmdm  49528  infsubc2  49536  infsubc2d  49537  oppfvalg  49601  reldmprcof1  49856  reldmprcof2  49857  dfinito4  49976  reldmlan2  50092  reldmran2  50093  termolmd  50145