Theorem dmeqd 5817

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

Syntax hints:   → wi 4   = wceq 1539  dom cdm 5590

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2710

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-3an 1088  df-tru 1542  df-fal 1552  df-ex 1783  df-sb 2069  df-clab 2717  df-cleq 2731  df-clel 2817  df-rab 3074  df-v 3435  df-dif 3891  df-un 3893  df-in 3895  df-ss 3905  df-nul 4258  df-if 4461  df-sn 4563  df-pr 4565  df-op 4569  df-br 5076  df-dm 5600

This theorem is referenced by:  dmxpid  5842  rneq  5848  dmxpss  6079  dmsnopss  6122  dmsnsnsn  6128  f10d  6759  fndmin  6931  fninfp  7055  fndifnfp  7057  ovmpt3rabdm  7537  elxp4  7778  1stval  7842  fo1st  7860  f1stres  7864  bropopvvv  7939  bropfvvvv  7941  mpocurryd  8094  errn  8529  xpassen  8862  xpdom2  8863  oicl  9297  oif  9298  hartogslem1  9310  cantnfdm  9431  cantnfval  9435  cantnf0  9442  cantnfres  9444  cnfcomlem  9466  hsmexlem4  10194  hsmexlem5  10195  axdc3lem2  10216  ttukeylem3  10276  hashfun  14161  s1dmALT  14323  swrdval  14365  swrd0  14380  s2dmALT  14630  s4dom  14641  dmtrclfv  14738  relexpnndm  14761  relexpdmg  14762  relexpdmd  14764  relexpnnrn  14765  relexpfld  14769  relexpaddg  14773  shftdm  14791  rlim  15213  ramval  16718  isstruct2  16859  setsvalg  16876  setsdm  16880  prdsval  17175  homfeqbas  17414  invf  17489  dfiso2  17493  oppciso  17502  cicsym  17525  sscfn1  17538  sscfn2  17539  isssc  17541  rescval  17548  rescval2  17549  issubc  17559  issubc2  17560  cofuval  17606  resfval  17616  resfval2  17617  resf1st  17618  estrreslem2  17864  prfval  17925  lubdm  18078  glbdm  18091  joindm  18102  meetdm  18116  islat  18160  isclat  18227  oduclatb  18234  gsumvalx  18369  cntzrcl  18942  f1omvdco2  19065  pmtrfrn  19075  symgsssg  19084  symgfisg  19085  symggen  19087  pmtrdifwrdellem3  19100  pmtrdifwrdel2lem1  19101  pmtrdifwrdel  19102  pmtrdifwrdel2  19103  psgnunilem1  19110  psgnunilem5  19111  psgnunilem2  19112  psgnunilem3  19113  psgneldm  19120  dmdprd  19610  dprdval  19615  dpjfval  19667  ablfaclem3  19699  cofipsgn  20807  elocv  20882  ishil  20934  dsmmval  20950  mpfrcl  21304  mamudm  21546  mavmuldm  21708  mavmul0g  21711  m1detdiag  21755  decpmatval0  21922  decpmatval  21923  pmatcollpw3lem  21941  iscnp2  22399  ptval  22730  ptcmplem2  23213  cnextfval  23222  tsmsval2  23290  ustbas2  23386  utopval  23393  tusval  23426  ucnval  23438  iscfilu  23449  psmetdmdm  23467  xmetdmdm  23497  blfvalps  23545  setsmstopn  23642  tmsval  23645  metuval  23714  tngtopn  23823  cfilfval  24437  caufval  24448  limcfval  25045  dvfval  25070  dvbsss  25075  perfdvf  25076  dvmptresicc  25089  dvn2bss  25103  dvnres  25104  dvcmul  25117  dvcmulf  25118  dvcj  25123  dvnfre  25125  dvexp  25126  dvmptres3  25129  dvmptcl  25132  dvmptadd  25133  dvmptmul  25134  dvmptres2  25135  dvmptcmul  25137  dvmptcj  25141  dvmptco  25145  rolle  25163  cmvth  25164  mvth  25165  dvlip  25166  dvlipcn  25167  dvlip2  25168  c1liplem1  25169  dveq0  25173  dv11cn  25174  dvle  25180  dvivthlem1  25181  dvivth  25183  dvne0  25184  lhop1lem  25186  lhop2  25188  lhop  25189  dvcnvrelem1  25190  dvcvx  25193  dvfsumle  25194  dvfsumge  25195  dvfsumabs  25196  dvmptrecl  25197  dvfsumlem2  25200  itgsubstlem  25221  taylfval  25527  tayl0  25530  dvtaylp  25538  dvntaylp  25539  dvntaylp0  25540  taylthlem1  25541  taylthlem2  25542  ulmdvlem1  25568  pserdv  25597  pige3ALT  25685  logtayl  25824  relogbf  25950  lgamgulmlem2  26188  perpln1  27080  isuhgr  27439  isushgr  27440  uhgreq12g  27444  isuhgrop  27449  uhgrun  27453  uhgrstrrepe  27457  isupgr  27463  upgrop  27473  isumgr  27474  upgr1e  27492  upgrun  27497  umgrun  27499  isuspgr  27531  isusgr  27532  isuspgrop  27540  isusgrop  27541  ausgrusgrb  27544  usgrstrrepe  27611  uspgr1e  27620  usgrexmpl  27639  issubgr  27647  uhgrspansubgrlem  27666  usgrexi  27817  vtxdgfval  27843  vtxdeqd  27853  vtxdun  27857  1loopgrvd0  27880  1hevtxdg0  27881  1hevtxdg1  27882  umgr2v2e  27901  umgr2v2evd2  27903  ewlksfval  27977  wksfval  27985  wlkres  28047  wlkp1  28058  eupths  28573  eupthres  28588  trlsegvdeglem4  28596  trlsegvdeglem5  28597  grporndm  28881  hmoval  29181  gsumhashmul  31325  symgcom2  31362  symgcntz  31363  pmtrcnel2  31368  cycpmco2f1  31400  cycpmrn  31419  tocyccntz  31420  smatrcl  31755  metidval  31849  pstmval  31854  prsssdm  31876  ordtrestNEW  31880  ofcfval  32075  ofcfval3  32079  brae  32218  braew  32219  faeval  32223  mbfmcst  32235  carsgval  32279  issibf  32309  sitmval  32325  0rrv  32427  dstrvprob  32447  fineqvac  33075  satfdm  33340  fmlafv  33351  fmla  33352  fmlasuc0  33355  satfdmfmla  33371  nosupdm  33916  nosupbday  33917  nosupres  33919  nosupbnd1lem1  33920  nosupbnd1  33926  nosupbnd2  33928  noinfdm  33931  noinfbday  33932  noinfbnd1  33941  noinfbnd2  33943  cnndvlem2  34727  bj-finsumval0  35465  cureq  35762  curf  35764  curunc  35768  sdclem2  35909  ismtyval  35967  isass  36013  isexid  36014  ismndo2  36041  exidreslem  36044  rngodm1dm2  36099  divrngcl  36124  isdrngo2  36125  isopos  37201  isatl  37320  dibffval  39161  dibfval  39162  conrel2d  41279  iunrelexp0  41317  dmtrclfvRP  41345  rntrclfvRP  41346  neicvgbex  41729  dvsconst  41955  expgrowth  41960  fnlimfvre  43222  dvsinax  43461  dvcosax  43474  dvbdfbdioolem1  43476  itgsinexplem1  43502  itgcoscmulx  43517  dirkeritg  43650  dirkercncflem2  43652  fourierdlem60  43714  fourierdlem61  43715  fourierdlem74  43728  fourierdlem75  43729  fourierdlem80  43734  fourierdlem94  43748  fourierdlem103  43757  fourierdlem104  43758  fourierdlem113  43767  dmvon  44151  ovnovollem1  44201  smflimlem3  44318  smflimlem4  44319  smflim  44322  smflim2  44350  smfpimcc  44352  smflimmpt  44354  smfsuplem2  44356  smfsuplem3  44357  smfsup  44358  smfsupmpt  44359  smfinflem  44361  smfinf  44362  smfinfmpt  44363  smflimsuplem1  44364  smflimsuplem2  44365  smflimsuplem3  44366  smflimsuplem4  44367  smflimsuplem7  44370  smflimsup  44372  smflimsupmpt  44373  smfliminf  44375  smfliminfmpt  44376  dfateq12d  44629  isomgr  45286  isomgreqve  45288  ushrisomgr  45304  upwlksfval  45308  mndpsuppss  45718  lubeldm2d  46263  glbeldm2d  46264  glbprlem  46270  isclatd  46280