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  6853  fndmin  7038  fninfp  7173  fndifnfp  7175  ovmpt3rabdm  7674  elxp4  7920  1stval  7989  fo1st  8007  f1stres  8011  bropopvvv  8088  bropfvvvv  8090  mpocurryd  8268  errn  8720  cureq  8869  curf  8870  xpassen  9070  xpdom2  9071  oicl  9502  oif  9503  hartogslem1  9515  cantnfdm  9644  cantnfval  9648  cantnf0  9655  cantnfres  9657  cnfcomlem  9679  hsmexlem4  10432  hsmexlem5  10433  axdc3lem2  10454  ttukeylem3  10514  hashfun  14503  s1dmALT  14678  swrdval  14712  swrd0  14729  s2dmALT  14980  s4dom  14991  dmtrclfv  15092  relexpnndm  15115  relexpdmg  15116  relexpdmd  15118  relexpnnrn  15119  relexpfld  15123  relexpaddg  15127  shftdm  15145  rlim  15583  ramval  17101  isstruct2  17242  setsvalg  17259  setsdm  17263  prdsval  17541  homfeqbas  17785  invf  17858  dfiso2  17862  oppciso  17871  cicsym  17894  sscfn1  17907  sscfn2  17908  isssc  17910  rescval  17917  rescval2  17918  issubc  17925  issubc2  17926  cofuval  17972  resfval  17982  resfval2  17983  resf1st  17984  estrreslem2  18227  prfval  18288  lubdm  18438  glbdm  18451  joindm  18462  meetdm  18476  islat  18522  isclat  18589  oduclatb  18596  gsumvalx  18779  mndpsuppss  18873  cntzrcl  19455  f1omvdco2  19576  pmtrfrn  19586  symgsssg  19595  symgfisg  19596  symggen  19598  pmtrdifwrdellem3  19611  pmtrdifwrdel2lem1  19612  pmtrdifwrdel  19613  pmtrdifwrdel2  19614  psgnunilem1  19621  psgnunilem5  19622  psgnunilem2  19623  psgnunilem3  19624  psgneldm  19631  dmdprd  20128  dprdval  20133  dpjfval  20185  ablfaclem3  20217  cofipsgn  21807  elocv  21882  ishil  21932  dsmmval  21948  mpfrcl  22302  mamudm  22618  mavmuldm  22773  mavmul0g  22776  m1detdiag  22820  decpmatval0  22990  decpmatval  22991  pmatcollpw3lem  23009  iscnp2  23465  ptval  23797  ptcmplem2  24280  cnextfval  24289  tsmsval2  24357  ustbas2  24452  utopval  24459  tusval  24492  ucnval  24503  iscfilu  24514  psmetdmdm  24532  xmetdmdm  24562  blfvalps  24610  setsmstopn  24705  tmsval  24708  metuval  24776  tngtopn  24877  cfilfval  25493  caufval  25504  limcfval  26100  dvfval  26125  dvbsss  26130  perfdvf  26131  dvmptresicc  26144  dvn2bss  26158  dvnres  26159  dvcmul  26172  dvcmulf  26173  dvcj  26178  dvnfre  26180  dvexp  26181  dvmptres3  26184  dvmptcl  26187  dvmptadd  26188  dvmptmul  26189  dvmptres2  26190  dvmptcmul  26192  dvmptcj  26196  dvmptco  26200  rolle  26218  cmvth  26219  mvth  26220  dvlip  26221  dvlipcn  26222  dvlip2  26223  c1liplem1  26224  dveq0  26228  dv11cn  26229  dvle  26235  dvivthlem1  26236  dvivth  26238  dvne0  26239  lhop1lem  26241  lhop2  26243  lhop  26244  dvcnvrelem1  26245  dvcvx  26248  dvfsumle  26249  dvfsumge  26250  dvfsumabs  26251  dvmptrecl  26252  dvfsumlem2  26255  itgsubstlem  26276  taylfval  26596  tayl0  26599  dvtaylp  26607  dvntaylp  26608  dvntaylp0  26609  taylthlem1  26610  taylthlem2  26611  ulmdvlem1  26637  pserdv  26666  pige3ALT  26758  logtayl  26898  relogbf  27029  lgamgulmlem2  27267  nosupdm  27941  nosupbday  27942  nosupres  27944  nosupbnd1lem1  27945  nosupbnd1  27951  nosupbnd2  27953  noinfdm  27956  noinfbday  27957  noinfbnd1  27966  noinfbnd2  27968  perpln1  29065  isuhgr  29518  isushgr  29519  uhgreq12g  29523  isuhgrop  29528  uhgrun  29532  uhgrstrrepe  29536  isupgr  29542  upgrop  29552  isumgr  29553  upgr1e  29571  upgrun  29576  umgrun  29578  isuspgr  29613  isusgr  29614  isuspgrop  29622  isusgrop  29623  ausgrusgrb  29626  usgrstrrepe  29696  uspgr1e  29705  issubgr  29732  uhgrspansubgrlem  29751  usgrexi  29902  vtxdgfval  29928  vtxdeqd  29938  vtxdun  29942  1loopgrvd0  29965  1hevtxdg0  29966  1hevtxdg1  29967  umgr2v2e  29986  umgr2v2evd2  29988  ewlksfval  30062  wksfval  30070  wlkres  30129  wlkp1  30140  eupths  30681  eupthres  30696  trlsegvdeglem4  30704  trlsegvdeglem5  30705  grporndm  30992  hmoval  31292  gsumhashmul  33508  symgcom2  33525  symgcntz  33526  pmtrcnel2  33531  cycpmco2f1  33565  cycpmrn  33584  tocyccntz  33585  fxpval  33606  fxpgaval  33608  1arithidomlem2  33947  1arithidom  33948  minplyval  34216  smatrcl  34307  metidval  34401  pstmval  34406  prsssdm  34428  ordtrestNEW  34432  ofcfval  34609  ofcfval3  34613  brae  34753  braew  34754  faeval  34758  mbfmcst  34771  carsgval  34815  issibf  34845  sitmval  34861  0rrv  34963  dstrvprob  34984  fineqvac  35643  satfdm  35949  fmlafv  35960  fmla  35961  fmlasuc0  35964  satfdmfmla  35980  cnndvlem2  37236  bj-finsumval0  38038  curunc  38357  sdclem2  38493  ismtyval  38551  isass  38597  isexid  38598  ismndo2  38625  exidreslem  38628  rngodm1dm2  38683  divrngcl  38708  isdrngo2  38709  cnvref4  39099  isopos  40054  isatl  40173  dibffval  42014  dibfval  42015  conrel2d  44505  iunrelexp0  44543  dmtrclfvRP  44571  rntrclfvRP  44572  neicvgbex  44953  dvsconst  45155  expgrowth  45160  fnlimfvre  46503  dvsinax  46742  dvcosax  46755  dvbdfbdioolem1  46757  itgsinexplem1  46783  itgcoscmulx  46798  dirkeritg  46931  dirkercncflem2  46933  fourierdlem60  46995  fourierdlem61  46996  fourierdlem74  47009  fourierdlem75  47010  fourierdlem80  47015  fourierdlem94  47029  fourierdlem103  47038  fourierdlem104  47039  fourierdlem113  47048  dmvon  47435  ovnovollem1  47485  smflimlem3  47602  smflimlem4  47603  smflim  47606  smflim2  47635  smfpimcc  47637  smflimmpt  47639  smfsuplem2  47641  smfsuplem3  47642  smfsup  47643  smfsupmpt  47644  smfinflem  47646  smfinf  47647  smfinfmpt  47648  smflimsuplem1  47649  smflimsuplem2  47650  smflimsuplem3  47651  smflimsuplem4  47652  smflimsuplem7  47655  smflimsup  47657  smflimsupmpt  47658  smfliminf  47660  smfliminfmpt  47661  tmachlem-agreefin  47777  dfateq12d  48015  isubgruhgr  48785  grimidvtxedg  48802  ushggricedg  48844  isubgrgrim  48846  stgrusgra  48876  gpgiedgdmel  48966  gpgusgra  48974  upwlksfval  49052  dmrnxp  49766  lubeldm2d  49885  glbeldm2d  49886  glbprlem  49892  isclatd  49910  isopropdlem  49967  dmdm  49980  infsubc2  49988  infsubc2d  49989  oppfvalg  50053  reldmprcof1  50308  reldmprcof2  50309  dfinito4  50428  reldmlan2  50544  reldmran2  50545  termolmd  50597