Theorem dmeqd 5881

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

Syntax hints:   → wi 4   = wceq 1560  dom cdm 5647

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1815  ax-4 1829  ax-5 1930  ax-6 1987  ax-7 2028  ax-8 2144  ax-9 2152  ax-ext 2734

This theorem depends on definitions:  df-bi 209  df-an 400  df-or 859  df-3an 1100  df-tru 1563  df-fal 1573  df-ex 1800  df-sb 2091  df-clab 2741  df-cleq 2754  df-clel 2837  df-rab 3415  df-v 3456  df-dif 3907  df-un 3909  df-ss 3921  df-nul 4286  df-if 4481  df-sn 4583  df-pr 4585  df-op 4589  df-br 5101  df-dm 5657

This theorem is referenced by:  dmxpid  5906  rneq  5912  dmxpss  6157  dmsnopss  6201  dmsnsnsn  6207  f10d  6841  fndmin  7026  fninfp  7158  fndifnfp  7160  ovmpt3rabdm  7655  elxp4  7903  1stval  7972  fo1st  7990  f1stres  7994  bropopvvv  8069  bropfvvvv  8071  mpocurryd  8249  errn  8701  xpassen  9043  xpdom2  9044  oicl  9477  oif  9478  hartogslem1  9490  cantnfdm  9619  cantnfval  9623  cantnf0  9630  cantnfres  9632  cnfcomlem  9654  hsmexlem4  10386  hsmexlem5  10387  axdc3lem2  10408  ttukeylem3  10468  hashfun  14450  s1dmALT  14623  swrdval  14657  swrd0  14672  s2dmALT  14921  s4dom  14932  dmtrclfv  15031  relexpnndm  15054  relexpdmg  15055  relexpdmd  15057  relexpnnrn  15058  relexpfld  15062  relexpaddg  15066  shftdm  15084  rlim  15522  ramval  17044  isstruct2  17185  setsvalg  17202  setsdm  17206  prdsval  17484  homfeqbas  17728  invf  17801  dfiso2  17805  oppciso  17814  cicsym  17837  sscfn1  17850  sscfn2  17851  isssc  17853  rescval  17860  rescval2  17861  issubc  17868  issubc2  17869  cofuval  17915  resfval  17925  resfval2  17926  resf1st  17927  estrreslem2  18170  prfval  18231  lubdm  18381  glbdm  18394  joindm  18405  meetdm  18419  islat  18465  isclat  18532  oduclatb  18539  gsumvalx  18710  mndpsuppss  18799  cntzrcl  19367  f1omvdco2  19488  pmtrfrn  19498  symgsssg  19507  symgfisg  19508  symggen  19510  pmtrdifwrdellem3  19523  pmtrdifwrdel2lem1  19524  pmtrdifwrdel  19525  pmtrdifwrdel2  19526  psgnunilem1  19533  psgnunilem5  19534  psgnunilem2  19535  psgnunilem3  19536  psgneldm  19543  dmdprd  20040  dprdval  20045  dpjfval  20097  ablfaclem3  20129  cofipsgn  21642  elocv  21717  ishil  21767  dsmmval  21783  mpfrcl  22135  mamudm  22452  mavmuldm  22607  mavmul0g  22610  m1detdiag  22654  decpmatval0  22821  decpmatval  22822  pmatcollpw3lem  22840  iscnp2  23296  ptval  23627  ptcmplem2  24110  cnextfval  24119  tsmsval2  24187  ustbas2  24282  utopval  24289  tusval  24322  ucnval  24333  iscfilu  24344  psmetdmdm  24362  xmetdmdm  24392  blfvalps  24440  setsmstopn  24535  tmsval  24538  metuval  24606  tngtopn  24707  cfilfval  25323  caufval  25334  limcfval  25931  dvfval  25956  dvbsss  25961  perfdvf  25962  dvmptresicc  25975  dvn2bss  25989  dvnres  25990  dvcmul  26003  dvcmulf  26004  dvcj  26009  dvnfre  26011  dvexp  26012  dvmptres3  26015  dvmptcl  26018  dvmptadd  26019  dvmptmul  26020  dvmptres2  26021  dvmptcmul  26023  dvmptcj  26027  dvmptco  26031  rolle  26049  cmvth  26050  mvth  26051  dvlip  26052  dvlipcn  26053  dvlip2  26054  c1liplem1  26055  dveq0  26059  dv11cn  26060  dvle  26066  dvivthlem1  26067  dvivth  26069  dvne0  26070  lhop1lem  26072  lhop2  26074  lhop  26075  dvcnvrelem1  26076  dvcvx  26079  dvfsumle  26080  dvfsumge  26081  dvfsumabs  26082  dvmptrecl  26083  dvfsumlem2  26086  itgsubstlem  26107  taylfval  26419  tayl0  26422  dvtaylp  26430  dvntaylp  26431  dvntaylp0  26432  taylthlem1  26433  taylthlem2  26434  ulmdvlem1  26460  pserdv  26489  pige3ALT  26582  logtayl  26722  relogbf  26853  lgamgulmlem2  27091  nosupdm  27765  nosupbday  27766  nosupres  27768  nosupbnd1lem1  27769  nosupbnd1  27775  nosupbnd2  27777  noinfdm  27780  noinfbday  27781  noinfbnd1  27790  noinfbnd2  27792  perpln1  28880  isuhgr  29258  isushgr  29259  uhgreq12g  29263  isuhgrop  29268  uhgrun  29272  uhgrstrrepe  29276  isupgr  29282  upgrop  29292  isumgr  29293  upgr1e  29311  upgrun  29316  umgrun  29318  isuspgr  29350  isusgr  29351  isuspgrop  29359  isusgrop  29360  ausgrusgrb  29363  usgrstrrepe  29433  uspgr1e  29442  issubgr  29469  uhgrspansubgrlem  29488  usgrexi  29639  vtxdgfval  29665  vtxdeqd  29675  vtxdun  29679  1loopgrvd0  29702  1hevtxdg0  29703  1hevtxdg1  29704  umgr2v2e  29723  umgr2v2evd2  29725  ewlksfval  29799  wksfval  29807  wlkres  29866  wlkp1  29877  eupths  30399  eupthres  30414  trlsegvdeglem4  30422  trlsegvdeglem5  30423  grporndm  30710  hmoval  31010  gsumhashmul  33244  symgcom2  33261  symgcntz  33262  pmtrcnel2  33267  cycpmco2f1  33301  cycpmrn  33320  tocyccntz  33321  fxpval  33342  fxpgaval  33344  1arithidomlem2  33729  1arithidom  33730  minplyval  33999  smatrcl  34090  metidval  34184  pstmval  34189  prsssdm  34211  ordtrestNEW  34215  ofcfval  34392  ofcfval3  34396  brae  34535  braew  34536  faeval  34540  mbfmcst  34553  carsgval  34597  issibf  34627  sitmval  34643  0rrv  34745  dstrvprob  34766  fineqvac  35409  satfdm  35716  fmlafv  35727  fmla  35728  fmlasuc0  35731  satfdmfmla  35747  cnndvlem2  36973  bj-finsumval0  37774  cureq  38092  curf  38094  curunc  38098  sdclem2  38238  ismtyval  38296  isass  38342  isexid  38343  ismndo2  38370  exidreslem  38373  rngodm1dm2  38428  divrngcl  38453  isdrngo2  38454  cnvref4  38846  isopos  39801  isatl  39920  dibffval  41761  dibfval  41762  conrel2d  44237  iunrelexp0  44275  dmtrclfvRP  44303  rntrclfvRP  44304  neicvgbex  44685  dvsconst  44903  expgrowth  44908  fnlimfvre  46245  dvsinax  46484  dvcosax  46497  dvbdfbdioolem1  46499  itgsinexplem1  46525  itgcoscmulx  46540  dirkeritg  46673  dirkercncflem2  46675  fourierdlem60  46737  fourierdlem61  46738  fourierdlem74  46751  fourierdlem75  46752  fourierdlem80  46757  fourierdlem94  46771  fourierdlem103  46780  fourierdlem104  46781  fourierdlem113  46790  dmvon  47177  ovnovollem1  47227  smflimlem3  47344  smflimlem4  47345  smflim  47348  smflim2  47377  smfpimcc  47379  smflimmpt  47381  smfsuplem2  47383  smfsuplem3  47384  smfsup  47385  smfsupmpt  47386  smfinflem  47388  smfinf  47389  smfinfmpt  47390  smflimsuplem1  47391  smflimsuplem2  47392  smflimsuplem3  47393  smflimsuplem4  47394  smflimsuplem7  47397  smflimsup  47399  smflimsupmpt  47400  smfliminf  47402  smfliminfmpt  47403  dfateq12d  47717  isubgruhgr  48487  grimidvtxedg  48504  ushggricedg  48546  isubgrgrim  48548  stgrusgra  48578  gpgiedgdmel  48668  gpgusgra  48676  upwlksfval  48754  dmrnxp  49455  lubeldm2d  49576  glbeldm2d  49577  glbprlem  49583  isclatd  49601  isopropdlem  49658  dmdm  49671  infsubc2  49679  infsubc2d  49680  oppfvalg  49744  reldmprcof1  49999  reldmprcof2  50000  dfinito4  50119  reldmlan2  50235  reldmran2  50236  termolmd  50288