Theorem dmeqd 5888

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

This proof depends on syntax axioms:   → wi 4   = wceq 1569  dom cdm 5651

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1572  df-fal 1582  df-ex 1812  df-sb 2099  df-clab 2739  df-cleq 2752  df-clel 2835  df-rab 3413  df-v 3452  df-ss 3897  df-dif 4046  df-un 4150  df-nul 4278  df-if 4482  df-sn 4585  df-pr 4587  df-op 4835  df-br 5103  df-dm 5661

This theorem is used by:  dmxpid  5913  rneq  5919  dmxpss  6165  dmsnopss  6218  dmsnsnsn  6224  f10d  6864  fndmin  7049  fninfp  7183  fndifnfp  7185  ovmpt3rabdm  7684  elxp4  7938  1stval  8007  fo1st  8025  f1stres  8029  bropopvvv  8105  bropfvvvv  8107  mpocurryd  8293  errn  8747  cureq  8896  curf  8897  xpassen  9097  xpdom2  9098  oicl  9530  oif  9531  hartogslem1  9543  cantnfdm  9672  cantnfval  9676  cantnf0  9683  cantnfres  9685  cnfcomlem  9707  hsmexlem4  10514  hsmexlem5  10515  axdc3lem2  10536  ttukeylem3  10596  hashfun  14589  s1dmALT  14765  swrdval  14799  swrd0  14816  s2dmALT  15068  s4dom  15079  dmtrclfv  15180  relexpnndm  15203  relexpdmg  15204  relexpdmd  15206  relexpnnrn  15207  relexpfld  15211  relexpaddg  15215  shftdm  15233  rlim  15671  ramval  17195  isstruct2  17336  setsvalg  17353  setsdm  17357  prdsval  17635  homfeqbas  17879  invf  17952  dfiso2  17956  oppciso  17965  cicsym  17988  sscfn1  18001  sscfn2  18002  isssc  18004  rescval  18011  rescval2  18012  issubc  18019  issubc2  18020  cofuval  18066  resfval  18076  resfval2  18077  resf1st  18078  estrreslem2  18321  prfval  18382  lubdm  18532  glbdm  18545  joindm  18556  meetdm  18570  islat  18616  isclat  18683  oduclatb  18690  gsumvalx  18874  mndpsuppss  18968  cntzrcl  19550  f1omvdco2  19671  pmtrfrn  19681  symgsssg  19690  symgfisg  19691  symggen  19693  pmtrdifwrdellem3  19706  pmtrdifwrdel2lem1  19707  pmtrdifwrdel  19708  pmtrdifwrdel2  19709  psgnunilem1  19716  psgnunilem5  19717  psgnunilem2  19718  psgnunilem3  19719  psgneldm  19726  dmdprd  20223  dprdval  20228  dpjfval  20280  ablfaclem3  20312  cofipsgn  21908  elocv  21983  ishil  22033  dsmmval  22049  mpfrcl  22403  mamudm  22719  mavmuldm  22874  mavmul0g  22877  m1detdiag  22921  decpmatval0  23091  decpmatval  23092  pmatcollpw3lem  23110  iscnp2  23566  ptval  23898  ptcmplem2  24381  cnextfval  24390  tsmsval2  24458  ustbas2  24553  utopval  24560  tusval  24593  ucnval  24604  iscfilu  24615  psmetdmdm  24633  xmetdmdm  24663  blfvalps  24711  setsmstopn  24806  tmsval  24809  metuval  24877  tngtopn  24978  cfilfval  25594  caufval  25605  limcfval  26201  dvfval  26226  dvbsss  26231  perfdvf  26232  dvmptresicc  26245  dvn2bss  26259  dvnres  26260  dvcmul  26273  dvcmulf  26274  dvcj  26279  dvnfre  26281  dvexp  26282  dvmptres3  26285  dvmptcl  26288  dvmptadd  26289  dvmptmul  26290  dvmptres2  26291  dvmptcmul  26293  dvmptcj  26297  dvmptco  26301  rolle  26319  cmvth  26320  mvth  26321  dvlip  26322  dvlipcn  26323  dvlip2  26324  c1liplem1  26325  dveq0  26329  dv11cn  26330  dvle  26336  dvivthlem1  26337  dvivth  26339  dvne0  26340  lhop1lem  26342  lhop2  26344  lhop  26345  dvcnvrelem1  26346  dvcvx  26349  dvfsumle  26350  dvfsumge  26351  dvfsumabs  26352  dvmptrecl  26353  dvfsumlem2  26356  itgsubstlem  26377  taylfval  26695  tayl0  26698  dvtaylp  26706  dvntaylp  26707  dvntaylp0  26708  taylthlem1  26709  taylthlem2  26710  ulmdvlem1  26736  pserdv  26765  pige3ALT  26857  logtayl  26997  relogbf  27128  lgamgulmlem2  27366  nosupdm  28070  nosupbday  28071  nosupres  28073  nosupbnd1lem1  28074  nosupbnd1  28080  nosupbnd2  28082  noinfdm  28085  noinfbday  28086  noinfbnd1  28095  noinfbnd2  28097  perpln1  29194  isuhgr  29647  isushgr  29648  uhgreq12g  29652  isuhgrop  29657  uhgrun  29661  uhgrstrrepe  29665  isupgr  29671  upgrop  29681  isumgr  29682  upgr1e  29700  upgrun  29705  umgrun  29707  isuspgr  29742  isusgr  29743  isuspgrop  29751  isusgrop  29752  ausgrusgrb  29755  usgrstrrepe  29825  uspgr1e  29834  issubgr  29861  uhgrspansubgrlem  29880  usgrexi  30031  vtxdgfval  30057  vtxdeqd  30067  vtxdun  30071  1loopgrvd0  30094  1hevtxdg0  30095  1hevtxdg1  30096  umgr2v2e  30115  umgr2v2evd2  30117  ewlksfval  30191  wksfval  30199  wlkres  30258  wlkp1  30269  eupths  30810  eupthres  30825  trlsegvdeglem4  30833  trlsegvdeglem5  30834  grporndm  31121  hmoval  31421  gsumhashmul  33678  symgcom2  33695  symgcntz  33696  pmtrcnel2  33701  cycpmco2f1  33735  cycpmrn  33754  tocyccntz  33755  fxpval  33776  fxpgaval  33778  1arithidomlem2  34118  1arithidom  34119  minplyval  34387  smatrcl  34478  metidval  34572  pstmval  34577  prsssdm  34599  ordtrestNEW  34603  ofcfval  34780  ofcfval3  34784  brae  34924  braew  34925  faeval  34929  mbfmcst  34941  carsgval  34985  issibf  35015  sitmval  35031  0rrv  35133  dstrvprob  35154  fineqvac  35844  satfdm  36224  fmlafv  36235  fmla  36236  fmlasuc0  36239  satfdmfmla  36255  cnndvlem2  37500  bj-finsumval0  38315  curunc  38634  sdclem2  38785  ismtyval  38843  isass  38889  isexid  38890  ismndo2  38917  exidreslem  38920  rngodm1dm2  38975  divrngcl  39000  isdrngo2  39001  cnvref4  39391  isopos  40346  isatl  40465  dibffval  42306  dibfval  42307  conrel2d  44773  iunrelexp0  44811  dmtrclfvRP  44839  rntrclfvRP  44840  neicvgbex  45221  dvsconst  45423  expgrowth  45428  fnlimfvre  46792  dvsinax  47031  dvcosax  47044  dvbdfbdioolem1  47046  itgsinexplem1  47072  itgcoscmulx  47087  dirkeritg  47220  dirkercncflem2  47222  fourierdlem60  47284  fourierdlem61  47285  fourierdlem74  47298  fourierdlem75  47299  fourierdlem80  47304  fourierdlem94  47318  fourierdlem103  47327  fourierdlem104  47328  fourierdlem113  47337  dmvon  47724  ovnovollem1  47774  smflimlem3  47891  smflimlem4  47892  smflim  47895  smflim2  47924  smfpimcc  47926  smflimmpt  47928  smfsuplem2  47930  smfsuplem3  47931  smfsup  47932  smfsupmpt  47933  smfinflem  47935  smfinf  47936  smfinfmpt  47937  smflimsuplem1  47938  smflimsuplem2  47939  smflimsuplem3  47940  smflimsuplem4  47941  smflimsuplem7  47944  smflimsup  47946  smflimsupmpt  47947  smfliminf  47949  smfliminfmpt  47950  tmachlem-agreefin  48066  dfateq12d  48304  isubgruhgr  49074  grimidvtxedg  49091  ushggricedg  49133  isubgrgrim  49135  stgrusgra  49165  gpgiedgdmel  49255  gpgusgra  49263  upwlksfval  49341  dmrnxp  50056  lubeldm2d  50180  glbeldm2d  50181  glbprlem  50187  isclatd  50205  isopropdlem  50262  dmdm  50275  infsubc2  50283  infsubc2d  50284  oppfvalg  50350  reldmprcof1  50624  reldmprcof2  50625  dfinito4  50744  termccofix  50779  reldmlan2  50908  reldmran2  50909  termolmd  50961