MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  dmeqd Structured version   Visualization version   GIF version

Theorem dmeqd 5248
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
StepHypRef Expression
1 dmeqd.1 . 2 (𝜑𝐴 = 𝐵)
2 dmeq 5246 . 2 (𝐴 = 𝐵 → dom 𝐴 = dom 𝐵)
31, 2syl 17 1 (𝜑 → dom 𝐴 = dom 𝐵)
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1475  dom cdm 5038
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590
This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-3an 1033  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-clab 2597  df-cleq 2603  df-clel 2606  df-nfc 2740  df-rab 2905  df-v 3175  df-dif 3543  df-un 3545  df-in 3547  df-ss 3554  df-nul 3875  df-if 4037  df-sn 4126  df-pr 4128  df-op 4132  df-br 4584  df-dm 5048
This theorem is referenced by:  dmxpid  5266  rneq  5272  dmxpss  5484  dmsnopss  5525  dmsnsnsn  5531  f10d  6082  fndmin  6232  fninfp  6345  fndifnfp  6347  ovmpt3rabdm  6790  elxp4  7003  1stval  7061  fo1st  7079  f1stres  7081  bropopvvv  7142  bropfvvvv  7144  suppsnop  7196  mpt2curryd  7282  errn  7651  xpassen  7939  xpdom2  7940  oicl  8317  oif  8318  hartogslem1  8330  cantnfdm  8444  cantnfval  8448  cantnf0  8455  cantnfres  8457  cnfcomlem  8479  hsmexlem4  9134  hsmexlem5  9135  axdc3lem2  9156  ttukeylem3  9216  hashfun  13084  s1dmALT  13242  swrdval  13269  swrd0  13286  s2dmALT  13503  s4dom  13514  dmtrclfv  13607  relexpnndm  13629  relexpdmg  13630  relexpnnrn  13633  relexpfld  13637  relexpaddg  13641  shftdm  13659  rlim  14074  ramval  15550  isstruct2  15704  setsvalg  15719  setsdm  15724  prdsval  15938  homfeqbas  16179  invf  16251  dfiso2  16255  oppciso  16264  cicsym  16287  sscfn1  16300  sscfn2  16301  isssc  16303  rescval  16310  rescval2  16311  issubc  16318  issubc2  16319  cofuval  16365  resfval  16375  resfval2  16376  resf1st  16377  estrreslem2  16601  prfval  16662  lubdm  16802  glbdm  16815  joindm  16826  meetdm  16840  islat  16870  isclat  16932  oduclatb  16967  gsumvalx  17093  cntzrcl  17583  f1omvdco2  17691  pmtrfrn  17701  symgsssg  17710  symgfisg  17711  symggen  17713  pmtrdifwrdellem3  17726  pmtrdifwrdel2lem1  17727  pmtrdifwrdel  17728  pmtrdifwrdel2  17729  psgnunilem1  17736  psgnunilem5  17737  psgnunilem2  17738  psgnunilem3  17739  psgneldm  17746  dmdprd  18220  dprdval  18225  dpjfval  18277  ablfaclem3  18309  mpfrcl  19339  zrhcofipsgn  19758  elocv  19831  ishil  19881  dsmmval  19897  mamudm  20013  mavmuldm  20175  mavmul0g  20178  m1detdiag  20222  decpmatval0  20388  decpmatval  20389  pmatcollpw3lem  20407  iscnp2  20853  ptval  21183  ptcmplem2  21667  cnextfval  21676  tsmsval2  21743  ustbas2  21839  utopval  21846  tusval  21880  ucnval  21891  iscfilu  21902  psmetdmdm  21920  xmetdmdm  21950  blfvalps  21998  setsmstopn  22093  tmsval  22096  metuval  22164  tngtopn  22264  cfilfval  22870  caufval  22881  limcfval  23442  dvfval  23467  dvbsss  23472  perfdvf  23473  dvn2bss  23499  dvnres  23500  dvcmul  23513  dvcmulf  23514  dvcj  23519  dvnfre  23521  dvexp  23522  dvmptres3  23525  dvmptcl  23528  dvmptadd  23529  dvmptmul  23530  dvmptres2  23531  dvmptcmul  23533  dvmptcj  23537  dvmptco  23541  rolle  23557  cmvth  23558  mvth  23559  dvlip  23560  dvlipcn  23561  dvlip2  23562  c1liplem1  23563  dveq0  23567  dv11cn  23568  dvle  23574  dvivthlem1  23575  dvivth  23577  dvne0  23578  lhop1lem  23580  lhop2  23582  lhop  23583  dvcnvrelem1  23584  dvcvx  23587  dvfsumle  23588  dvfsumge  23589  dvfsumabs  23590  dvmptrecl  23591  dvfsumlem2  23594  itgsubstlem  23615  taylfval  23917  tayl0  23920  dvtaylp  23928  dvntaylp  23929  dvntaylp0  23930  taylthlem1  23931  taylthlem2  23932  ulmdvlem1  23958  pserdv  23987  pige3  24073  logtayl  24206  relogbf  24329  lgamgulmlem2  24556  perpln1  25405  isuhgr  25726  isushgr  25727  uhgreq12g  25731  isuhgrop  25736  uhgrun  25740  uhgrstrrepe  25745  isupgr  25751  isumgr  25761  upgr1e  25779  upgrun  25784  umgrun  25786  isushgra  25830  isumgra  25844  clwwlknprop  26300  2wlkonot3v  26402  2spthonot3v  26403  vdgrfval  26422  iseupa  26492  grporndm  26748  hmoval  27049  smatrcl  29190  metidval  29261  pstmval  29266  prsssdm  29291  ordtrestNEW  29295  ofcfval  29487  ofcfval3  29491  brae  29631  braew  29632  faeval  29636  mbfmcst  29648  carsgval  29692  issibf  29722  sitmval  29738  0rrv  29840  dstrvprob  29860  cnndvlem2  31699  bj-finsumval0  32324  cureq  32555  curf  32557  curunc  32561  sdclem2  32708  ismtyval  32769  isass  32815  isexid  32816  ismndo2  32843  exidreslem  32846  rngodm1dm2  32901  divrngcl  32926  isdrngo2  32927  isopos  33485  isatl  33604  dibffval  35447  dibfval  35448  conrel2d  36975  iunrelexp0  37013  dmtrclfvRP  37041  rntrclfvRP  37042  neicvgbex  37430  dvsconst  37551  expgrowth  37556  fnlimfvre  38741  dvsinax  38801  dvmptresicc  38809  dvcosax  38816  dvbdfbdioolem1  38818  itgsinexplem1  38845  itgcoscmulx  38861  dirkeritg  38995  dirkercncflem2  38997  fourierdlem60  39059  fourierdlem61  39060  fourierdlem74  39073  fourierdlem75  39074  fourierdlem80  39079  fourierdlem94  39093  fourierdlem103  39102  fourierdlem104  39103  fourierdlem113  39112  dmvon  39496  ovnovollem1  39546  smflimlem3  39659  smflimlem4  39660  smflim  39663  dfateq12d  39858  uhgruhgra  40375  uhgrauhgr  40376  isuspgr  40382  isusgr  40383  isusgrop  40392  ausgrusgrb  40395  uspgr1e  40470  usgrexmpl  40487  issubgr  40495  uhgrspansubgrlem  40514  usgrexi  40661  vtxdgfval  40683  vtxdeqd  40692  vtxdun  40696  1loopgrvd0  40719  1hevtxdg0  40720  1hevtxdg1  40721  umgr2v2e  40741  umgr2v2evd2  40743  ewlksfval  40803  1wlksfval  40811  wlksfval  40812  1wlkres  40879  1wlkp1  40890  eupths  41367  eupthres  41383  trlsegvdeglem4  41391  trlsegvdeglem5  41392  mndpsuppss  41946
  Copyright terms: Public domain W3C validator