Theorem dmeqd 5916

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

Syntax hints:   → wi 4   = wceq 1540  dom cdm 5685

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2065  df-clab 2715  df-cleq 2729  df-clel 2816  df-rab 3437  df-v 3482  df-dif 3954  df-un 3956  df-ss 3968  df-nul 4334  df-if 4526  df-sn 4627  df-pr 4629  df-op 4633  df-br 5144  df-dm 5695

This theorem is referenced by:  dmxpid  5941  rneq  5947  dmxpss  6191  dmsnopss  6234  dmsnsnsn  6240  f10d  6882  fndmin  7065  fninfp  7194  fndifnfp  7196  ovmpt3rabdm  7692  elxp4  7944  1stval  8016  fo1st  8034  f1stres  8038  bropopvvv  8115  bropfvvvv  8117  mpocurryd  8294  errn  8767  xpassen  9106  xpdom2  9107  oicl  9569  oif  9570  hartogslem1  9582  cantnfdm  9704  cantnfval  9708  cantnf0  9715  cantnfres  9717  cnfcomlem  9739  hsmexlem4  10469  hsmexlem5  10470  axdc3lem2  10491  ttukeylem3  10551  hashfun  14476  s1dmALT  14647  swrdval  14681  swrd0  14696  s2dmALT  14947  s4dom  14958  dmtrclfv  15057  relexpnndm  15080  relexpdmg  15081  relexpdmd  15083  relexpnnrn  15084  relexpfld  15088  relexpaddg  15092  shftdm  15110  rlim  15531  ramval  17046  isstruct2  17186  setsvalg  17203  setsdm  17207  prdsval  17500  homfeqbas  17739  invf  17812  dfiso2  17816  oppciso  17825  cicsym  17848  sscfn1  17861  sscfn2  17862  isssc  17864  rescval  17871  rescval2  17872  issubc  17880  issubc2  17881  cofuval  17927  resfval  17937  resfval2  17938  resf1st  17939  estrreslem2  18183  prfval  18244  lubdm  18396  glbdm  18409  joindm  18420  meetdm  18434  islat  18478  isclat  18545  oduclatb  18552  gsumvalx  18689  mndpsuppss  18778  cntzrcl  19345  f1omvdco2  19466  pmtrfrn  19476  symgsssg  19485  symgfisg  19486  symggen  19488  pmtrdifwrdellem3  19501  pmtrdifwrdel2lem1  19502  pmtrdifwrdel  19503  pmtrdifwrdel2  19504  psgnunilem1  19511  psgnunilem5  19512  psgnunilem2  19513  psgnunilem3  19514  psgneldm  19521  dmdprd  20018  dprdval  20023  dpjfval  20075  ablfaclem3  20107  cofipsgn  21611  elocv  21686  ishil  21738  dsmmval  21754  mpfrcl  22109  mamudm  22399  mavmuldm  22556  mavmul0g  22559  m1detdiag  22603  decpmatval0  22770  decpmatval  22771  pmatcollpw3lem  22789  iscnp2  23247  ptval  23578  ptcmplem2  24061  cnextfval  24070  tsmsval2  24138  ustbas2  24234  utopval  24241  tusval  24274  ucnval  24286  iscfilu  24297  psmetdmdm  24315  xmetdmdm  24345  blfvalps  24393  setsmstopn  24490  tmsval  24493  metuval  24562  tngtopn  24671  cfilfval  25298  caufval  25309  limcfval  25907  dvfval  25932  dvbsss  25937  perfdvf  25938  dvmptresicc  25951  dvn2bss  25966  dvnres  25967  dvcmul  25981  dvcmulf  25982  dvcj  25988  dvnfre  25990  dvexp  25991  dvmptres3  25994  dvmptcl  25997  dvmptadd  25998  dvmptmul  25999  dvmptres2  26000  dvmptcmul  26002  dvmptcj  26006  dvmptco  26010  rolle  26028  cmvth  26029  cmvthOLD  26030  mvth  26031  dvlip  26032  dvlipcn  26033  dvlip2  26034  c1liplem1  26035  dveq0  26039  dv11cn  26040  dvle  26046  dvivthlem1  26047  dvivth  26049  dvne0  26050  lhop1lem  26052  lhop2  26054  lhop  26055  dvcnvrelem1  26056  dvcvx  26059  dvfsumle  26060  dvfsumleOLD  26061  dvfsumge  26062  dvfsumabs  26063  dvmptrecl  26064  dvfsumlem2  26067  dvfsumlem2OLD  26068  itgsubstlem  26089  taylfval  26400  tayl0  26403  dvtaylp  26412  dvntaylp  26413  dvntaylp0  26414  taylthlem1  26415  taylthlem2  26416  taylthlem2OLD  26417  ulmdvlem1  26443  pserdv  26473  pige3ALT  26562  logtayl  26702  relogbf  26834  lgamgulmlem2  27073  nosupdm  27749  nosupbday  27750  nosupres  27752  nosupbnd1lem1  27753  nosupbnd1  27759  nosupbnd2  27761  noinfdm  27764  noinfbday  27765  noinfbnd1  27774  noinfbnd2  27776  perpln1  28718  isuhgr  29077  isushgr  29078  uhgreq12g  29082  isuhgrop  29087  uhgrun  29091  uhgrstrrepe  29095  isupgr  29101  upgrop  29111  isumgr  29112  upgr1e  29130  upgrun  29135  umgrun  29137  isuspgr  29169  isusgr  29170  isuspgrop  29178  isusgrop  29179  ausgrusgrb  29182  usgrstrrepe  29252  uspgr1e  29261  issubgr  29288  uhgrspansubgrlem  29307  usgrexi  29458  vtxdgfval  29485  vtxdeqd  29495  vtxdun  29499  1loopgrvd0  29522  1hevtxdg0  29523  1hevtxdg1  29524  umgr2v2e  29543  umgr2v2evd2  29545  ewlksfval  29619  wksfval  29627  wlkres  29688  wlkp1  29699  eupths  30219  eupthres  30234  trlsegvdeglem4  30242  trlsegvdeglem5  30243  grporndm  30529  hmoval  30829  gsumhashmul  33064  symgcom2  33104  symgcntz  33105  pmtrcnel2  33110  cycpmco2f1  33144  cycpmrn  33163  tocyccntz  33164  1arithidomlem2  33564  1arithidom  33565  minplyval  33748  smatrcl  33795  metidval  33889  pstmval  33894  prsssdm  33916  ordtrestNEW  33920  ofcfval  34099  ofcfval3  34103  brae  34242  braew  34243  faeval  34247  mbfmcst  34261  carsgval  34305  issibf  34335  sitmval  34351  0rrv  34453  dstrvprob  34474  fineqvac  35111  satfdm  35374  fmlafv  35385  fmla  35386  fmlasuc0  35389  satfdmfmla  35405  cnndvlem2  36539  bj-finsumval0  37286  cureq  37603  curf  37605  curunc  37609  sdclem2  37749  ismtyval  37807  isass  37853  isexid  37854  ismndo2  37881  exidreslem  37884  rngodm1dm2  37939  divrngcl  37964  isdrngo2  37965  cnvref4  38351  isopos  39181  isatl  39300  dibffval  41142  dibfval  41143  conrel2d  43677  iunrelexp0  43715  dmtrclfvRP  43743  rntrclfvRP  43744  neicvgbex  44125  dvsconst  44349  expgrowth  44354  fnlimfvre  45689  dvsinax  45928  dvcosax  45941  dvbdfbdioolem1  45943  itgsinexplem1  45969  itgcoscmulx  45984  dirkeritg  46117  dirkercncflem2  46119  fourierdlem60  46181  fourierdlem61  46182  fourierdlem74  46195  fourierdlem75  46196  fourierdlem80  46201  fourierdlem94  46215  fourierdlem103  46224  fourierdlem104  46225  fourierdlem113  46234  dmvon  46621  ovnovollem1  46671  smflimlem3  46788  smflimlem4  46789  smflim  46792  smflim2  46821  smfpimcc  46823  smflimmpt  46825  smfsuplem2  46827  smfsuplem3  46828  smfsup  46829  smfsupmpt  46830  smfinflem  46832  smfinf  46833  smfinfmpt  46834  smflimsuplem1  46835  smflimsuplem2  46836  smflimsuplem3  46837  smflimsuplem4  46838  smflimsuplem7  46841  smflimsup  46843  smflimsupmpt  46844  smfliminf  46846  smfliminfmpt  46847  dfateq12d  47138  isubgruhgr  47854  grimidvtxedg  47876  ushggricedg  47896  isubgrgrim  47897  stgrusgra  47926  gpgusgra  48012  upwlksfval  48051  lubeldm2d  48855  glbeldm2d  48856  glbprlem  48862  isclatd  48872