Theorem dmeqd 5617

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

Syntax hints:   → wi 4   = wceq 1507  dom cdm 5400

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1758  ax-4 1772  ax-5 1869  ax-6 1928  ax-7 1964  ax-8 2050  ax-9 2057  ax-10 2077  ax-11 2091  ax-12 2104  ax-ext 2745

This theorem depends on definitions:  df-bi 199  df-an 388  df-or 834  df-3an 1070  df-tru 1510  df-ex 1743  df-nf 1747  df-sb 2014  df-clab 2754  df-cleq 2765  df-clel 2840  df-nfc 2912  df-rab 3091  df-v 3411  df-dif 3828  df-un 3830  df-in 3832  df-ss 3839  df-nul 4174  df-if 4345  df-sn 4436  df-pr 4438  df-op 4442  df-br 4924  df-dm 5410

This theorem is referenced by:  dmxpid  5636  rneq  5642  dmxpss  5862  dmsnopss  5904  dmsnsnsn  5910  f10d  6471  fndmin  6634  fninfp  6753  fndifnfp  6755  ovmpt3rabdm  7216  elxp4  7436  1stval  7496  fo1st  7514  f1stres  7518  bropopvvv  7586  bropfvvvv  7588  suppsnop  7640  mpocurryd  7731  errn  8103  xpassen  8399  xpdom2  8400  oicl  8780  oif  8781  hartogslem1  8793  cantnfdm  8913  cantnfval  8917  cantnf0  8924  cantnfres  8926  cnfcomlem  8948  hsmexlem4  9641  hsmexlem5  9642  axdc3lem2  9663  ttukeylem3  9723  hashfun  13601  s1dmALT  13762  swrdval  13796  swrd0  13816  s2dmALT  14122  s4dom  14133  dmtrclfv  14229  relexpnndm  14251  relexpdmg  14252  relexpnnrn  14255  relexpfld  14259  relexpaddg  14263  shftdm  14281  rlim  14703  ramval  16190  isstruct2  16339  setsvalg  16358  setsdm  16363  prdsval  16574  homfeqbas  16814  invf  16886  dfiso2  16890  oppciso  16899  cicsym  16922  sscfn1  16935  sscfn2  16936  isssc  16938  rescval  16945  rescval2  16946  issubc  16953  issubc2  16954  cofuval  17000  resfval  17010  resfval2  17011  resf1st  17012  estrreslem2  17236  prfval  17297  lubdm  17437  glbdm  17450  joindm  17461  meetdm  17475  islat  17505  isclat  17567  oduclatb  17602  gsumvalx  17728  cntzrcl  18218  f1omvdco2  18327  pmtrfrn  18337  symgsssg  18346  symgfisg  18347  symggen  18349  pmtrdifwrdellem3  18362  pmtrdifwrdel2lem1  18363  pmtrdifwrdel  18364  pmtrdifwrdel2  18365  psgnunilem1  18372  psgnunilem5  18373  psgnunilem5OLD  18374  psgnunilem2  18375  psgnunilem3  18376  psgneldm  18383  dmdprd  18860  dprdval  18865  dpjfval  18917  ablfaclem3  18949  mpfrcl  20001  cofipsgn  20429  elocv  20504  ishil  20554  dsmmval  20570  mamudm  20691  mavmuldm  20853  mavmul0g  20856  m1detdiag  20900  decpmatval0  21066  decpmatval  21067  pmatcollpw3lem  21085  iscnp2  21541  ptval  21872  ptcmplem2  22355  cnextfval  22364  tsmsval2  22431  ustbas2  22527  utopval  22534  tusval  22568  ucnval  22579  iscfilu  22590  psmetdmdm  22608  xmetdmdm  22638  blfvalps  22686  setsmstopn  22781  tmsval  22784  metuval  22852  tngtopn  22952  cfilfval  23560  caufval  23571  limcfval  24163  dvfval  24188  dvbsss  24193  perfdvf  24194  dvn2bss  24220  dvnres  24221  dvcmul  24234  dvcmulf  24235  dvcj  24240  dvnfre  24242  dvexp  24243  dvmptres3  24246  dvmptcl  24249  dvmptadd  24250  dvmptmul  24251  dvmptres2  24252  dvmptcmul  24254  dvmptcj  24258  dvmptco  24262  rolle  24280  cmvth  24281  mvth  24282  dvlip  24283  dvlipcn  24284  dvlip2  24285  c1liplem1  24286  dveq0  24290  dv11cn  24291  dvle  24297  dvivthlem1  24298  dvivth  24300  dvne0  24301  lhop1lem  24303  lhop2  24305  lhop  24306  dvcnvrelem1  24307  dvcvx  24310  dvfsumle  24311  dvfsumge  24312  dvfsumabs  24313  dvmptrecl  24314  dvfsumlem2  24317  itgsubstlem  24338  taylfval  24640  tayl0  24643  dvtaylp  24651  dvntaylp  24652  dvntaylp0  24653  taylthlem1  24654  taylthlem2  24655  ulmdvlem1  24681  pserdv  24710  pige3ALT  24798  logtayl  24934  relogbf  25060  lgamgulmlem2  25299  perpln1  26188  isuhgr  26538  isushgr  26539  uhgreq12g  26543  isuhgrop  26548  uhgrun  26552  uhgrstrrepe  26556  isupgr  26562  upgrop  26572  isumgr  26573  upgr1e  26591  upgrun  26596  umgrun  26598  isuspgr  26630  isusgr  26631  isuspgrop  26639  isusgrop  26640  ausgrusgrb  26643  usgrstrrepe  26710  uspgr1e  26719  usgrexmpl  26738  issubgr  26746  uhgrspansubgrlem  26765  usgrexi  26916  vtxdgfval  26942  vtxdeqd  26952  vtxdun  26956  1loopgrvd0  26979  1hevtxdg0  26980  1hevtxdg1  26981  umgr2v2e  27000  umgr2v2evd2  27002  ewlksfval  27076  wksfval  27084  wlkres  27146  wlkresOLD  27148  wlkp1  27159  eupths  27719  eupthresOLD  27734  eupthres  27735  trlsegvdeglem4  27743  trlsegvdeglem5  27744  grporndm  28054  hmoval  28354  smatrcl  30660  metidval  30731  pstmval  30736  prsssdm  30761  ordtrestNEW  30765  ofcfval  30958  ofcfval3  30962  brae  31102  braew  31103  faeval  31107  mbfmcst  31119  carsgval  31163  issibf  31193  sitmval  31209  0rrv  31312  dstrvprob  31332  nosupdm  32665  nosupbday  32666  nosupres  32668  nosupbnd1lem1  32669  nosupbnd1  32675  nosupbnd2  32677  cnndvlem2  33337  bj-finsumval0  33965  cureq  34257  curf  34259  curunc  34263  sdclem2  34407  ismtyval  34468  isass  34514  isexid  34515  ismndo2  34542  exidreslem  34545  rngodm1dm2  34600  divrngcl  34625  isdrngo2  34626  isopos  35709  isatl  35828  dibffval  37669  dibfval  37670  conrel2d  39317  iunrelexp0  39355  dmtrclfvRP  39383  rntrclfvRP  39384  neicvgbex  39770  dvsconst  40022  expgrowth  40027  fnlimfvre  41332  dvsinax  41573  dvmptresicc  41580  dvcosax  41587  dvbdfbdioolem1  41589  itgsinexplem1  41615  itgcoscmulx  41630  dirkeritg  41764  dirkercncflem2  41766  fourierdlem60  41828  fourierdlem61  41829  fourierdlem74  41842  fourierdlem75  41843  fourierdlem80  41848  fourierdlem94  41862  fourierdlem103  41871  fourierdlem104  41872  fourierdlem113  41881  dmvon  42265  ovnovollem1  42315  smflimlem3  42426  smflimlem4  42427  smflim  42430  smflim2  42457  smfpimcc  42459  smflimmpt  42461  smfsuplem2  42463  smfsuplem3  42464  smfsup  42465  smfsupmpt  42466  smfinflem  42468  smfinf  42469  smfinfmpt  42470  smflimsuplem1  42471  smflimsuplem2  42472  smflimsuplem3  42473  smflimsuplem4  42474  smflimsuplem7  42477  smflimsup  42479  smflimsupmpt  42480  smfliminf  42482  smfliminfmpt  42483  dfateq12d  42677  isomgr  43296  isomgreqve  43298  ushrisomgr  43314  upwlksfval  43318  mndpsuppss  43725