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

Theorem dmeqd 5761
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 5759 . 2 (𝐴 = 𝐵 → dom 𝐴 = dom 𝐵)
31, 2syl 17 1 (𝜑 → dom 𝐴 = dom 𝐵)
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1538  dom cdm 5542
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1971  ax-7 2016  ax-8 2117  ax-9 2125  ax-10 2146  ax-11 2162  ax-12 2179  ax-ext 2796
This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3an 1086  df-tru 1541  df-ex 1782  df-nf 1786  df-sb 2071  df-clab 2803  df-cleq 2817  df-clel 2896  df-nfc 2964  df-v 3482  df-un 3924  df-in 3926  df-ss 3936  df-sn 4551  df-pr 4553  df-op 4557  df-br 5053  df-dm 5552
This theorem is referenced by:  dmxpid  5787  rneq  5793  dmxpss  6015  dmsnopss  6058  dmsnsnsn  6064  f10d  6639  fndmin  6806  fninfp  6927  fndifnfp  6929  ovmpt3rabdm  7398  elxp4  7622  1stval  7686  fo1st  7704  f1stres  7708  bropopvvv  7781  bropfvvvv  7783  mpocurryd  7931  errn  8307  xpassen  8607  xpdom2  8608  oicl  8990  oif  8991  hartogslem1  9003  cantnfdm  9124  cantnfval  9128  cantnf0  9135  cantnfres  9137  cnfcomlem  9159  hsmexlem4  9849  hsmexlem5  9850  axdc3lem2  9871  ttukeylem3  9931  hashfun  13803  s1dmALT  13963  swrdval  14005  swrd0  14020  s2dmALT  14270  s4dom  14281  dmtrclfv  14378  relexpnndm  14400  relexpdmg  14401  relexpnnrn  14404  relexpfld  14408  relexpaddg  14412  shftdm  14430  rlim  14852  ramval  16342  isstruct2  16493  setsvalg  16512  setsdm  16517  prdsval  16728  homfeqbas  16966  invf  17038  dfiso2  17042  oppciso  17051  cicsym  17074  sscfn1  17087  sscfn2  17088  isssc  17090  rescval  17097  rescval2  17098  issubc  17105  issubc2  17106  cofuval  17152  resfval  17162  resfval2  17163  resf1st  17164  estrreslem2  17388  prfval  17449  lubdm  17589  glbdm  17602  joindm  17613  meetdm  17627  islat  17657  isclat  17719  oduclatb  17754  gsumvalx  17886  cntzrcl  18457  f1omvdco2  18576  pmtrfrn  18586  symgsssg  18595  symgfisg  18596  symggen  18598  pmtrdifwrdellem3  18611  pmtrdifwrdel2lem1  18612  pmtrdifwrdel  18613  pmtrdifwrdel2  18614  psgnunilem1  18621  psgnunilem5  18622  psgnunilem2  18623  psgnunilem3  18624  psgneldm  18631  dmdprd  19120  dprdval  19125  dpjfval  19177  ablfaclem3  19209  mpfrcl  20298  cofipsgn  20737  elocv  20812  ishil  20862  dsmmval  20878  mamudm  20999  mavmuldm  21159  mavmul0g  21162  m1detdiag  21206  decpmatval0  21372  decpmatval  21373  pmatcollpw3lem  21391  iscnp2  21847  ptval  22178  ptcmplem2  22661  cnextfval  22670  tsmsval2  22738  ustbas2  22834  utopval  22841  tusval  22875  ucnval  22886  iscfilu  22897  psmetdmdm  22915  xmetdmdm  22945  blfvalps  22993  setsmstopn  23088  tmsval  23091  metuval  23159  tngtopn  23259  cfilfval  23871  caufval  23882  limcfval  24478  dvfval  24503  dvbsss  24508  perfdvf  24509  dvmptresicc  24522  dvn2bss  24536  dvnres  24537  dvcmul  24550  dvcmulf  24551  dvcj  24556  dvnfre  24558  dvexp  24559  dvmptres3  24562  dvmptcl  24565  dvmptadd  24566  dvmptmul  24567  dvmptres2  24568  dvmptcmul  24570  dvmptcj  24574  dvmptco  24578  rolle  24596  cmvth  24597  mvth  24598  dvlip  24599  dvlipcn  24600  dvlip2  24601  c1liplem1  24602  dveq0  24606  dv11cn  24607  dvle  24613  dvivthlem1  24614  dvivth  24616  dvne0  24617  lhop1lem  24619  lhop2  24621  lhop  24622  dvcnvrelem1  24623  dvcvx  24626  dvfsumle  24627  dvfsumge  24628  dvfsumabs  24629  dvmptrecl  24630  dvfsumlem2  24633  itgsubstlem  24654  taylfval  24957  tayl0  24960  dvtaylp  24968  dvntaylp  24969  dvntaylp0  24970  taylthlem1  24971  taylthlem2  24972  ulmdvlem1  24998  pserdv  25027  pige3ALT  25115  logtayl  25254  relogbf  25380  lgamgulmlem2  25618  perpln1  26507  isuhgr  26856  isushgr  26857  uhgreq12g  26861  isuhgrop  26866  uhgrun  26870  uhgrstrrepe  26874  isupgr  26880  upgrop  26890  isumgr  26891  upgr1e  26909  upgrun  26914  umgrun  26916  isuspgr  26948  isusgr  26949  isuspgrop  26957  isusgrop  26958  ausgrusgrb  26961  usgrstrrepe  27028  uspgr1e  27037  usgrexmpl  27056  issubgr  27064  uhgrspansubgrlem  27083  usgrexi  27234  vtxdgfval  27260  vtxdeqd  27270  vtxdun  27274  1loopgrvd0  27297  1hevtxdg0  27298  1hevtxdg1  27299  umgr2v2e  27318  umgr2v2evd2  27320  ewlksfval  27394  wksfval  27402  wlkres  27463  wlkp1  27474  eupths  27988  eupthres  28003  trlsegvdeglem4  28011  trlsegvdeglem5  28012  grporndm  28296  hmoval  28596  symgcom2  30760  symgcntz  30761  pmtrcnel2  30766  cycpmco2f1  30798  cycpmrn  30817  tocyccntz  30818  smatrcl  31121  metidval  31190  pstmval  31195  prsssdm  31217  ordtrestNEW  31221  ofcfval  31414  ofcfval3  31418  brae  31557  braew  31558  faeval  31562  mbfmcst  31574  carsgval  31618  issibf  31648  sitmval  31664  0rrv  31766  dstrvprob  31786  satfdm  32673  fmlafv  32684  fmla  32685  fmlasuc0  32688  satfdmfmla  32704  nosupdm  33261  nosupbday  33262  nosupres  33264  nosupbnd1lem1  33265  nosupbnd1  33271  nosupbnd2  33273  cnndvlem2  33934  bj-finsumval0  34645  cureq  34978  curf  34980  curunc  34984  sdclem2  35125  ismtyval  35183  isass  35229  isexid  35230  ismndo2  35257  exidreslem  35260  rngodm1dm2  35315  divrngcl  35340  isdrngo2  35341  isopos  36421  isatl  36540  dibffval  38381  dibfval  38382  conrel2d  40281  iunrelexp0  40319  dmtrclfvRP  40347  rntrclfvRP  40348  neicvgbex  40734  dvsconst  40954  expgrowth  40959  fnlimfvre  42242  dvsinax  42481  dvcosax  42494  dvbdfbdioolem1  42496  itgsinexplem1  42522  itgcoscmulx  42537  dirkeritg  42670  dirkercncflem2  42672  fourierdlem60  42734  fourierdlem61  42735  fourierdlem74  42748  fourierdlem75  42749  fourierdlem80  42754  fourierdlem94  42768  fourierdlem103  42777  fourierdlem104  42778  fourierdlem113  42787  dmvon  43171  ovnovollem1  43221  smflimlem3  43332  smflimlem4  43333  smflim  43336  smflim2  43363  smfpimcc  43365  smflimmpt  43367  smfsuplem2  43369  smfsuplem3  43370  smfsup  43371  smfsupmpt  43372  smfinflem  43374  smfinf  43375  smfinfmpt  43376  smflimsuplem1  43377  smflimsuplem2  43378  smflimsuplem3  43379  smflimsuplem4  43380  smflimsuplem7  43383  smflimsup  43385  smflimsupmpt  43386  smfliminf  43388  smfliminfmpt  43389  dfateq12d  43608  isomgr  44267  isomgreqve  44269  ushrisomgr  44285  upwlksfval  44289  mndpsuppss  44699
  Copyright terms: Public domain W3C validator