Theorem dmeqd 5738

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

Syntax hints:   → wi 4   = wceq 1538  dom cdm 5519

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 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-10 2142  ax-11 2158  ax-12 2175  ax-ext 2770

This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3an 1086  df-tru 1541  df-ex 1782  df-nf 1786  df-sb 2070  df-clab 2777  df-cleq 2791  df-clel 2870  df-nfc 2938  df-v 3443  df-un 3886  df-in 3888  df-ss 3898  df-sn 4526  df-pr 4528  df-op 4532  df-br 5031  df-dm 5529

This theorem is referenced by:  dmxpid  5764  rneq  5770  dmxpss  5995  dmsnopss  6038  dmsnsnsn  6044  f10d  6623  fndmin  6792  fninfp  6913  fndifnfp  6915  ovmpt3rabdm  7384  elxp4  7609  1stval  7673  fo1st  7691  f1stres  7695  bropopvvv  7768  bropfvvvv  7770  mpocurryd  7918  errn  8294  xpassen  8594  xpdom2  8595  oicl  8977  oif  8978  hartogslem1  8990  cantnfdm  9111  cantnfval  9115  cantnf0  9122  cantnfres  9124  cnfcomlem  9146  hsmexlem4  9840  hsmexlem5  9841  axdc3lem2  9862  ttukeylem3  9922  hashfun  13794  s1dmALT  13954  swrdval  13996  swrd0  14011  s2dmALT  14261  s4dom  14272  dmtrclfv  14369  relexpnndm  14392  relexpdmg  14393  relexpdmd  14395  relexpnnrn  14396  relexpfld  14400  relexpaddg  14404  shftdm  14422  rlim  14844  ramval  16334  isstruct2  16485  setsvalg  16504  setsdm  16509  prdsval  16720  homfeqbas  16958  invf  17030  dfiso2  17034  oppciso  17043  cicsym  17066  sscfn1  17079  sscfn2  17080  isssc  17082  rescval  17089  rescval2  17090  issubc  17097  issubc2  17098  cofuval  17144  resfval  17154  resfval2  17155  resf1st  17156  estrreslem2  17380  prfval  17441  lubdm  17581  glbdm  17594  joindm  17605  meetdm  17619  islat  17649  isclat  17711  oduclatb  17746  gsumvalx  17878  cntzrcl  18449  f1omvdco2  18568  pmtrfrn  18578  symgsssg  18587  symgfisg  18588  symggen  18590  pmtrdifwrdellem3  18603  pmtrdifwrdel2lem1  18604  pmtrdifwrdel  18605  pmtrdifwrdel2  18606  psgnunilem1  18613  psgnunilem5  18614  psgnunilem2  18615  psgnunilem3  18616  psgneldm  18623  dmdprd  19113  dprdval  19118  dpjfval  19170  ablfaclem3  19202  cofipsgn  20282  elocv  20357  ishil  20407  dsmmval  20423  mpfrcl  20757  mamudm  20995  mavmuldm  21155  mavmul0g  21158  m1detdiag  21202  decpmatval0  21369  decpmatval  21370  pmatcollpw3lem  21388  iscnp2  21844  ptval  22175  ptcmplem2  22658  cnextfval  22667  tsmsval2  22735  ustbas2  22831  utopval  22838  tusval  22872  ucnval  22883  iscfilu  22894  psmetdmdm  22912  xmetdmdm  22942  blfvalps  22990  setsmstopn  23085  tmsval  23088  metuval  23156  tngtopn  23256  cfilfval  23868  caufval  23879  limcfval  24475  dvfval  24500  dvbsss  24505  perfdvf  24506  dvmptresicc  24519  dvn2bss  24533  dvnres  24534  dvcmul  24547  dvcmulf  24548  dvcj  24553  dvnfre  24555  dvexp  24556  dvmptres3  24559  dvmptcl  24562  dvmptadd  24563  dvmptmul  24564  dvmptres2  24565  dvmptcmul  24567  dvmptcj  24571  dvmptco  24575  rolle  24593  cmvth  24594  mvth  24595  dvlip  24596  dvlipcn  24597  dvlip2  24598  c1liplem1  24599  dveq0  24603  dv11cn  24604  dvle  24610  dvivthlem1  24611  dvivth  24613  dvne0  24614  lhop1lem  24616  lhop2  24618  lhop  24619  dvcnvrelem1  24620  dvcvx  24623  dvfsumle  24624  dvfsumge  24625  dvfsumabs  24626  dvmptrecl  24627  dvfsumlem2  24630  itgsubstlem  24651  taylfval  24954  tayl0  24957  dvtaylp  24965  dvntaylp  24966  dvntaylp0  24967  taylthlem1  24968  taylthlem2  24969  ulmdvlem1  24995  pserdv  25024  pige3ALT  25112  logtayl  25251  relogbf  25377  lgamgulmlem2  25615  perpln1  26504  isuhgr  26853  isushgr  26854  uhgreq12g  26858  isuhgrop  26863  uhgrun  26867  uhgrstrrepe  26871  isupgr  26877  upgrop  26887  isumgr  26888  upgr1e  26906  upgrun  26911  umgrun  26913  isuspgr  26945  isusgr  26946  isuspgrop  26954  isusgrop  26955  ausgrusgrb  26958  usgrstrrepe  27025  uspgr1e  27034  usgrexmpl  27053  issubgr  27061  uhgrspansubgrlem  27080  usgrexi  27231  vtxdgfval  27257  vtxdeqd  27267  vtxdun  27271  1loopgrvd0  27294  1hevtxdg0  27295  1hevtxdg1  27296  umgr2v2e  27315  umgr2v2evd2  27317  ewlksfval  27391  wksfval  27399  wlkres  27460  wlkp1  27471  eupths  27985  eupthres  28000  trlsegvdeglem4  28008  trlsegvdeglem5  28009  grporndm  28293  hmoval  28593  gsumhashmul  30741  symgcom2  30778  symgcntz  30779  pmtrcnel2  30784  cycpmco2f1  30816  cycpmrn  30835  tocyccntz  30836  smatrcl  31149  metidval  31243  pstmval  31248  prsssdm  31270  ordtrestNEW  31274  ofcfval  31467  ofcfval3  31471  brae  31610  braew  31611  faeval  31615  mbfmcst  31627  carsgval  31671  issibf  31701  sitmval  31717  0rrv  31819  dstrvprob  31839  satfdm  32729  fmlafv  32740  fmla  32741  fmlasuc0  32744  satfdmfmla  32760  nosupdm  33317  nosupbday  33318  nosupres  33320  nosupbnd1lem1  33321  nosupbnd1  33327  nosupbnd2  33329  cnndvlem2  33990  bj-finsumval0  34700  cureq  35033  curf  35035  curunc  35039  sdclem2  35180  ismtyval  35238  isass  35284  isexid  35285  ismndo2  35312  exidreslem  35315  rngodm1dm2  35370  divrngcl  35395  isdrngo2  35396  isopos  36476  isatl  36595  dibffval  38436  dibfval  38437  conrel2d  40365  iunrelexp0  40403  dmtrclfvRP  40431  rntrclfvRP  40432  neicvgbex  40815  dvsconst  41034  expgrowth  41039  fnlimfvre  42316  dvsinax  42555  dvcosax  42568  dvbdfbdioolem1  42570  itgsinexplem1  42596  itgcoscmulx  42611  dirkeritg  42744  dirkercncflem2  42746  fourierdlem60  42808  fourierdlem61  42809  fourierdlem74  42822  fourierdlem75  42823  fourierdlem80  42828  fourierdlem94  42842  fourierdlem103  42851  fourierdlem104  42852  fourierdlem113  42861  dmvon  43245  ovnovollem1  43295  smflimlem3  43406  smflimlem4  43407  smflim  43410  smflim2  43437  smfpimcc  43439  smflimmpt  43441  smfsuplem2  43443  smfsuplem3  43444  smfsup  43445  smfsupmpt  43446  smfinflem  43448  smfinf  43449  smfinfmpt  43450  smflimsuplem1  43451  smflimsuplem2  43452  smflimsuplem3  43453  smflimsuplem4  43454  smflimsuplem7  43457  smflimsup  43459  smflimsupmpt  43460  smfliminf  43462  smfliminfmpt  43463  dfateq12d  43682  isomgr  44341  isomgreqve  44343  ushrisomgr  44359  upwlksfval  44363  mndpsuppss  44773