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

Theorem dmeqd 5232
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 5230 . 2 (𝐴 = 𝐵 → dom 𝐴 = dom 𝐵)
31, 2syl 17 1 (𝜑 → dom 𝐴 = dom 𝐵)
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1474  dom cdm 5025
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1712  ax-4 1727  ax-5 1826  ax-6 1874  ax-7 1921  ax-10 2005  ax-11 2020  ax-12 2032  ax-13 2229  ax-ext 2586
This theorem depends on definitions:  df-bi 195  df-or 383  df-an 384  df-3an 1032  df-tru 1477  df-ex 1695  df-nf 1700  df-sb 1867  df-clab 2593  df-cleq 2599  df-clel 2602  df-nfc 2736  df-rab 2901  df-v 3171  df-dif 3539  df-un 3541  df-in 3543  df-ss 3550  df-nul 3871  df-if 4033  df-sn 4122  df-pr 4124  df-op 4128  df-br 4575  df-dm 5035
This theorem is referenced by:  dmxpid  5250  rneq  5256  dmxpss  5467  dmsnopss  5508  dmsnsnsn  5514  f10d  6064  fndmin  6214  fninfp  6320  fndifnfp  6322  ovmpt3rabdm  6764  elxp4  6977  1stval  7035  fo1st  7053  f1stres  7055  bropopvvv  7116  bropfvvvv  7118  suppsnop  7170  mpt2curryd  7256  errn  7625  xpassen  7913  xpdom2  7914  oicl  8291  oif  8292  hartogslem1  8304  cantnfdm  8418  cantnfval  8422  cantnf0  8429  cantnfres  8431  cnfcomlem  8453  hsmexlem4  9108  hsmexlem5  9109  axdc3lem2  9130  ttukeylem3  9190  hashfun  13033  s1dmALT  13185  swrdval  13212  swrd0  13229  s2dmALT  13446  s4dom  13457  dmtrclfv  13550  relexpnndm  13572  relexpdmg  13573  relexpnnrn  13576  relexpfld  13580  relexpaddg  13584  shftdm  13602  rlim  14017  ramval  15493  isstruct2  15647  setsvalg  15662  setsdm  15667  prdsval  15881  homfeqbas  16122  invf  16194  dfiso2  16198  oppciso  16207  cicsym  16230  sscfn1  16243  sscfn2  16244  isssc  16246  rescval  16253  rescval2  16254  issubc  16261  issubc2  16262  cofuval  16308  resfval  16318  resfval2  16319  resf1st  16320  estrreslem2  16544  prfval  16605  lubdm  16745  glbdm  16758  joindm  16769  meetdm  16783  islat  16813  isclat  16875  oduclatb  16910  gsumvalx  17036  cntzrcl  17526  f1omvdco2  17634  pmtrfrn  17644  symgsssg  17653  symgfisg  17654  symggen  17656  pmtrdifwrdellem3  17669  pmtrdifwrdel2lem1  17670  pmtrdifwrdel  17671  pmtrdifwrdel2  17672  psgnunilem1  17679  psgnunilem5  17680  psgnunilem2  17681  psgnunilem3  17682  psgneldm  17689  dmdprd  18163  dprdval  18168  dpjfval  18220  ablfaclem3  18252  mpfrcl  19282  zrhcofipsgn  19700  elocv  19770  ishil  19820  dsmmval  19836  mamudm  19952  mavmuldm  20114  mavmul0g  20117  m1detdiag  20161  decpmatval0  20327  decpmatval  20328  pmatcollpw3lem  20346  iscnp2  20792  ptval  21122  ptcmplem2  21606  cnextfval  21615  tsmsval2  21682  ustbas2  21778  utopval  21785  tusval  21819  ucnval  21830  iscfilu  21841  psmetdmdm  21859  xmetdmdm  21888  blfvalps  21936  setsmstopn  22031  tmsval  22034  metuval  22102  tngtopn  22199  cfilfval  22785  caufval  22796  limcfval  23356  dvfval  23381  dvbsss  23386  perfdvf  23387  dvn2bss  23413  dvnres  23414  dvcmul  23427  dvcmulf  23428  dvcj  23433  dvnfre  23435  dvexp  23436  dvmptres3  23439  dvmptcl  23442  dvmptadd  23443  dvmptmul  23444  dvmptres2  23445  dvmptcmul  23447  dvmptcj  23451  dvmptco  23455  rolle  23471  cmvth  23472  mvth  23473  dvlip  23474  dvlipcn  23475  dvlip2  23476  c1liplem1  23477  dveq0  23481  dv11cn  23482  dvle  23488  dvivthlem1  23489  dvivth  23491  dvne0  23492  lhop1lem  23494  lhop2  23496  lhop  23497  dvcnvrelem1  23498  dvcvx  23501  dvfsumle  23502  dvfsumge  23503  dvfsumabs  23504  dvmptrecl  23505  dvfsumlem2  23508  itgsubstlem  23529  taylfval  23831  tayl0  23834  dvtaylp  23842  dvntaylp  23843  dvntaylp0  23844  taylthlem1  23845  taylthlem2  23846  ulmdvlem1  23872  pserdv  23901  pige3  23987  logtayl  24120  relogbf  24243  lgamgulmlem2  24470  perpln1  25320  isushgra  25593  isumgra  25607  clwwlknprop  26063  2wlkonot3v  26165  2spthonot3v  26166  vdgrfval  26185  iseupa  26255  grporndm  26511  vcoprneOLD  26597  hmoval  26852  smatrcl  28993  metidval  29064  pstmval  29069  prsssdm  29094  ordtrestNEW  29098  ofcfval  29290  ofcfval3  29294  brae  29434  braew  29435  faeval  29439  mbfmcst  29451  carsgval  29495  issibf  29525  sitmval  29541  0rrv  29643  dstrvprob  29663  cnndvlem2  31502  bj-finsumval0  32124  cureq  32355  curf  32357  curunc  32361  sdclem2  32508  ismtyval  32569  isass  32615  isexid  32616  ismndo2  32643  exidreslem  32646  rngodm1dm2  32701  divrngcl  32726  isdrngo2  32727  isopos  33285  isatl  33404  dibffval  35247  dibfval  35248  conrel2d  36775  iunrelexp0  36813  dmtrclfvRP  36841  rntrclfvRP  36842  neicvgbex  37230  dvsconst  37351  expgrowth  37356  fnlimfvre  38542  dvsinax  38602  dvmptresicc  38610  dvcosax  38617  dvbdfbdioolem1  38619  itgsinexplem1  38646  itgcoscmulx  38662  dirkeritg  38796  dirkercncflem2  38798  fourierdlem60  38860  fourierdlem61  38861  fourierdlem74  38874  fourierdlem75  38875  fourierdlem80  38880  fourierdlem94  38894  fourierdlem103  38903  fourierdlem104  38904  fourierdlem113  38913  dmvon  39297  ovnovollem1  39347  smflimlem3  39460  smflimlem4  39461  smflim  39464  dfateq12d  39660  isuhgr  40281  isushgr  40282  uhgreq12g  40286  uhgruhgra  40291  uhgrauhgr  40292  isuhgrop  40294  uhgrun  40298  uhgrstrrepe  40303  isupgr  40309  isumgr  40319  upgr1e  40337  upgrun  40342  umgrun  40344  isuspgr  40381  isusgr  40382  isusgrop  40391  ausgrusgrb  40394  uspgr1e  40469  usgrexmpl  40486  issubgr  40494  uhgrspansubgrlem  40513  usgrexi  40660  vtxdgfval  40682  vtxdeqd  40691  vtxdun  40695  1loopgrvd0  40718  1hevtxdg0  40719  1hevtxdg1  40720  umgr2v2e  40740  umgr2v2evd2  40742  ewlksfval  40802  1wlksfval  40810  wlksfval  40811  1wlkres  40878  1wlkp1  40889  eupths  41366  eupthres  41382  trlsegvdeglem4  41390  trlsegvdeglem5  41391  mndpsuppss  41945
  Copyright terms: Public domain W3C validator