Theorem dmeqd 5889

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

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

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 2732

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 2739  df-cleq 2752  df-clel 2835  df-rab 3413  df-v 3452  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 5665

This theorem is used by:  dmxpid  5914  rneq  5920  dmxpss  6164  dmsnopss  6210  dmsnsnsn  6216  f10d  6852  fndmin  7037  fninfp  7172  fndifnfp  7174  ovmpt3rabdm  7673  elxp4  7919  1stval  7988  fo1st  8006  f1stres  8010  bropopvvv  8087  bropfvvvv  8089  mpocurryd  8267  errn  8719  cureq  8868  curf  8869  xpassen  9069  xpdom2  9070  oicl  9501  oif  9502  hartogslem1  9514  cantnfdm  9643  cantnfval  9647  cantnf0  9654  cantnfres  9656  cnfcomlem  9678  hsmexlem4  10431  hsmexlem5  10432  axdc3lem2  10453  ttukeylem3  10513  hashfun  14502  s1dmALT  14677  swrdval  14711  swrd0  14728  s2dmALT  14979  s4dom  14990  dmtrclfv  15091  relexpnndm  15114  relexpdmg  15115  relexpdmd  15117  relexpnnrn  15118  relexpfld  15122  relexpaddg  15126  shftdm  15144  rlim  15582  ramval  17100  isstruct2  17241  setsvalg  17258  setsdm  17262  prdsval  17540  homfeqbas  17784  invf  17857  dfiso2  17861  oppciso  17870  cicsym  17893  sscfn1  17906  sscfn2  17907  isssc  17909  rescval  17916  rescval2  17917  issubc  17924  issubc2  17925  cofuval  17971  resfval  17981  resfval2  17982  resf1st  17983  estrreslem2  18226  prfval  18287  lubdm  18437  glbdm  18450  joindm  18461  meetdm  18475  islat  18521  isclat  18588  oduclatb  18595  gsumvalx  18778  mndpsuppss  18872  cntzrcl  19454  f1omvdco2  19575  pmtrfrn  19585  symgsssg  19594  symgfisg  19595  symggen  19597  pmtrdifwrdellem3  19610  pmtrdifwrdel2lem1  19611  pmtrdifwrdel  19612  pmtrdifwrdel2  19613  psgnunilem1  19620  psgnunilem5  19621  psgnunilem2  19622  psgnunilem3  19623  psgneldm  19630  dmdprd  20127  dprdval  20132  dpjfval  20184  ablfaclem3  20216  cofipsgn  21806  elocv  21881  ishil  21931  dsmmval  21947  mpfrcl  22301  mamudm  22617  mavmuldm  22772  mavmul0g  22775  m1detdiag  22819  decpmatval0  22989  decpmatval  22990  pmatcollpw3lem  23008  iscnp2  23464  ptval  23796  ptcmplem2  24279  cnextfval  24288  tsmsval2  24356  ustbas2  24451  utopval  24458  tusval  24491  ucnval  24502  iscfilu  24513  psmetdmdm  24531  xmetdmdm  24561  blfvalps  24609  setsmstopn  24704  tmsval  24707  metuval  24775  tngtopn  24876  cfilfval  25492  caufval  25503  limcfval  26099  dvfval  26124  dvbsss  26129  perfdvf  26130  dvmptresicc  26143  dvn2bss  26157  dvnres  26158  dvcmul  26171  dvcmulf  26172  dvcj  26177  dvnfre  26179  dvexp  26180  dvmptres3  26183  dvmptcl  26186  dvmptadd  26187  dvmptmul  26188  dvmptres2  26189  dvmptcmul  26191  dvmptcj  26195  dvmptco  26199  rolle  26217  cmvth  26218  mvth  26219  dvlip  26220  dvlipcn  26221  dvlip2  26222  c1liplem1  26223  dveq0  26227  dv11cn  26228  dvle  26234  dvivthlem1  26235  dvivth  26237  dvne0  26238  lhop1lem  26240  lhop2  26242  lhop  26243  dvcnvrelem1  26244  dvcvx  26247  dvfsumle  26248  dvfsumge  26249  dvfsumabs  26250  dvmptrecl  26251  dvfsumlem2  26254  itgsubstlem  26275  taylfval  26595  tayl0  26598  dvtaylp  26606  dvntaylp  26607  dvntaylp0  26608  taylthlem1  26609  taylthlem2  26610  ulmdvlem1  26636  pserdv  26665  pige3ALT  26757  logtayl  26897  relogbf  27028  lgamgulmlem2  27266  nosupdm  27940  nosupbday  27941  nosupres  27943  nosupbnd1lem1  27944  nosupbnd1  27950  nosupbnd2  27952  noinfdm  27955  noinfbday  27956  noinfbnd1  27965  noinfbnd2  27967  perpln1  29064  isuhgr  29517  isushgr  29518  uhgreq12g  29522  isuhgrop  29527  uhgrun  29531  uhgrstrrepe  29535  isupgr  29541  upgrop  29551  isumgr  29552  upgr1e  29570  upgrun  29575  umgrun  29577  isuspgr  29612  isusgr  29613  isuspgrop  29621  isusgrop  29622  ausgrusgrb  29625  usgrstrrepe  29695  uspgr1e  29704  issubgr  29731  uhgrspansubgrlem  29750  usgrexi  29901  vtxdgfval  29927  vtxdeqd  29937  vtxdun  29941  1loopgrvd0  29964  1hevtxdg0  29965  1hevtxdg1  29966  umgr2v2e  29985  umgr2v2evd2  29987  ewlksfval  30061  wksfval  30069  wlkres  30128  wlkp1  30139  eupths  30680  eupthres  30695  trlsegvdeglem4  30703  trlsegvdeglem5  30704  grporndm  30991  hmoval  31291  gsumhashmul  33507  symgcom2  33524  symgcntz  33525  pmtrcnel2  33530  cycpmco2f1  33564  cycpmrn  33583  tocyccntz  33584  fxpval  33605  fxpgaval  33607  1arithidomlem2  33946  1arithidom  33947  minplyval  34215  smatrcl  34306  metidval  34400  pstmval  34405  prsssdm  34427  ordtrestNEW  34431  ofcfval  34608  ofcfval3  34612  brae  34752  braew  34753  faeval  34757  mbfmcst  34770  carsgval  34814  issibf  34844  sitmval  34860  0rrv  34962  dstrvprob  34983  fineqvac  35642  satfdm  35948  fmlafv  35959  fmla  35960  fmlasuc0  35963  satfdmfmla  35979  cnndvlem2  37235  bj-finsumval0  38037  curunc  38356  sdclem2  38492  ismtyval  38550  isass  38596  isexid  38597  ismndo2  38624  exidreslem  38627  rngodm1dm2  38682  divrngcl  38707  isdrngo2  38708  cnvref4  39098  isopos  40053  isatl  40172  dibffval  42013  dibfval  42014  conrel2d  44504  iunrelexp0  44542  dmtrclfvRP  44570  rntrclfvRP  44571  neicvgbex  44952  dvsconst  45154  expgrowth  45159  fnlimfvre  46502  dvsinax  46741  dvcosax  46754  dvbdfbdioolem1  46756  itgsinexplem1  46782  itgcoscmulx  46797  dirkeritg  46930  dirkercncflem2  46932  fourierdlem60  46994  fourierdlem61  46995  fourierdlem74  47008  fourierdlem75  47009  fourierdlem80  47014  fourierdlem94  47028  fourierdlem103  47037  fourierdlem104  47038  fourierdlem113  47047  dmvon  47434  ovnovollem1  47484  smflimlem3  47601  smflimlem4  47602  smflim  47605  smflim2  47634  smfpimcc  47636  smflimmpt  47638  smfsuplem2  47640  smfsuplem3  47641  smfsup  47642  smfsupmpt  47643  smfinflem  47645  smfinf  47646  smfinfmpt  47647  smflimsuplem1  47648  smflimsuplem2  47649  smflimsuplem3  47650  smflimsuplem4  47651  smflimsuplem7  47654  smflimsup  47656  smflimsupmpt  47657  smfliminf  47659  smfliminfmpt  47660  tmachlem-agreefin  47776  dfateq12d  48014  isubgruhgr  48784  grimidvtxedg  48801  ushggricedg  48843  isubgrgrim  48845  stgrusgra  48875  gpgiedgdmel  48965  gpgusgra  48973  upwlksfval  49051  dmrnxp  49765  lubeldm2d  49884  glbeldm2d  49885  glbprlem  49891  isclatd  49909  isopropdlem  49966  dmdm  49979  infsubc2  49987  infsubc2d  49988  oppfvalg  50052  reldmprcof1  50307  reldmprcof2  50308  dfinito4  50427  reldmlan2  50543  reldmran2  50544  termolmd  50596