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

Theorem dmeqd 5324
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 5322 . 2 (𝐴 = 𝐵 → dom 𝐴 = dom 𝐵)
31, 2syl 17 1 (𝜑 → dom 𝐴 = dom 𝐵)
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1482  dom cdm 5112
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1721  ax-4 1736  ax-5 1838  ax-6 1887  ax-7 1934  ax-9 1998  ax-10 2018  ax-11 2033  ax-12 2046  ax-13 2245  ax-ext 2601
This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3an 1039  df-tru 1485  df-ex 1704  df-nf 1709  df-sb 1880  df-clab 2608  df-cleq 2614  df-clel 2617  df-nfc 2752  df-rab 2920  df-v 3200  df-dif 3575  df-un 3577  df-in 3579  df-ss 3586  df-nul 3914  df-if 4085  df-sn 4176  df-pr 4178  df-op 4182  df-br 4652  df-dm 5122
This theorem is referenced by:  dmxpid  5343  rneq  5349  dmxpss  5563  dmsnopss  5605  dmsnsnsn  5611  f10d  6168  fndmin  6322  fninfp  6437  fndifnfp  6439  ovmpt3rabdm  6889  elxp4  7107  1stval  7167  fo1st  7185  f1stres  7187  bropopvvv  7252  bropfvvvv  7254  suppsnop  7306  mpt2curryd  7392  errn  7761  xpassen  8051  xpdom2  8052  oicl  8431  oif  8432  hartogslem1  8444  cantnfdm  8558  cantnfval  8562  cantnf0  8569  cantnfres  8571  cnfcomlem  8593  hsmexlem4  9248  hsmexlem5  9249  axdc3lem2  9270  ttukeylem3  9330  hashfun  13219  s1dmALT  13384  swrdval  13411  swrd0  13428  s2dmALT  13647  s4dom  13658  dmtrclfv  13753  relexpnndm  13775  relexpdmg  13776  relexpnnrn  13779  relexpfld  13783  relexpaddg  13787  shftdm  13805  rlim  14220  ramval  15706  isstruct2  15861  setsvalg  15881  setsdm  15886  prdsval  16109  homfeqbas  16350  invf  16422  dfiso2  16426  oppciso  16435  cicsym  16458  sscfn1  16471  sscfn2  16472  isssc  16474  rescval  16481  rescval2  16482  issubc  16489  issubc2  16490  cofuval  16536  resfval  16546  resfval2  16547  resf1st  16548  estrreslem2  16772  prfval  16833  lubdm  16973  glbdm  16986  joindm  16997  meetdm  17011  islat  17041  isclat  17103  oduclatb  17138  gsumvalx  17264  cntzrcl  17754  f1omvdco2  17862  pmtrfrn  17872  symgsssg  17881  symgfisg  17882  symggen  17884  pmtrdifwrdellem3  17897  pmtrdifwrdel2lem1  17898  pmtrdifwrdel  17899  pmtrdifwrdel2  17900  psgnunilem1  17907  psgnunilem5  17908  psgnunilem2  17909  psgnunilem3  17910  psgneldm  17917  dmdprd  18391  dprdval  18396  dpjfval  18448  ablfaclem3  18480  mpfrcl  19512  zrhcofipsgn  19933  elocv  20006  ishil  20056  dsmmval  20072  mamudm  20188  mavmuldm  20350  mavmul0g  20353  m1detdiag  20397  decpmatval0  20563  decpmatval  20564  pmatcollpw3lem  20582  iscnp2  21037  ptval  21367  ptcmplem2  21851  cnextfval  21860  tsmsval2  21927  ustbas2  22023  utopval  22030  tusval  22064  ucnval  22075  iscfilu  22086  psmetdmdm  22104  xmetdmdm  22134  blfvalps  22182  setsmstopn  22277  tmsval  22280  metuval  22348  tngtopn  22448  cfilfval  23056  caufval  23067  limcfval  23630  dvfval  23655  dvbsss  23660  perfdvf  23661  dvn2bss  23687  dvnres  23688  dvcmul  23701  dvcmulf  23702  dvcj  23707  dvnfre  23709  dvexp  23710  dvmptres3  23713  dvmptcl  23716  dvmptadd  23717  dvmptmul  23718  dvmptres2  23719  dvmptcmul  23721  dvmptcj  23725  dvmptco  23729  rolle  23747  cmvth  23748  mvth  23749  dvlip  23750  dvlipcn  23751  dvlip2  23752  c1liplem1  23753  dveq0  23757  dv11cn  23758  dvle  23764  dvivthlem1  23765  dvivth  23767  dvne0  23768  lhop1lem  23770  lhop2  23772  lhop  23773  dvcnvrelem1  23774  dvcvx  23777  dvfsumle  23778  dvfsumge  23779  dvfsumabs  23780  dvmptrecl  23781  dvfsumlem2  23784  itgsubstlem  23805  taylfval  24107  tayl0  24110  dvtaylp  24118  dvntaylp  24119  dvntaylp0  24120  taylthlem1  24121  taylthlem2  24122  ulmdvlem1  24148  pserdv  24177  pige3  24263  logtayl  24400  relogbf  24523  lgamgulmlem2  24750  perpln1  25599  isuhgr  25949  isushgr  25950  uhgreq12g  25954  isuhgrop  25959  uhgrun  25963  uhgrstrrepe  25967  isupgr  25973  upgrop  25983  isumgr  25984  upgr1e  26002  upgrun  26007  umgrun  26009  isuspgr  26041  isusgr  26042  isuspgrop  26050  isusgrop  26051  ausgrusgrb  26054  usgrstrrepe  26121  uspgr1e  26130  usgrexmpl  26149  issubgr  26157  uhgrspansubgrlem  26176  usgrexi  26331  vtxdgfval  26357  vtxdeqd  26367  vtxdun  26371  1loopgrvd0  26394  1hevtxdg0  26395  1hevtxdg1  26396  umgr2v2e  26415  umgr2v2evd2  26417  ewlksfval  26491  wksfval  26499  wlkres  26561  wlkp1  26572  eupths  27053  eupthres  27068  trlsegvdeglem4  27076  trlsegvdeglem5  27077  grporndm  27348  hmoval  27649  smatrcl  29847  metidval  29918  pstmval  29923  prsssdm  29948  ordtrestNEW  29952  ofcfval  30145  ofcfval3  30149  brae  30289  braew  30290  faeval  30294  mbfmcst  30306  carsgval  30350  issibf  30380  sitmval  30396  0rrv  30498  dstrvprob  30518  nosupdm  31834  nosupbday  31835  nosupres  31837  nosupbnd1lem1  31838  nosupbnd1  31844  nosupbnd2  31846  cnndvlem2  32513  bj-finsumval0  33127  cureq  33365  curf  33367  curunc  33371  sdclem2  33518  ismtyval  33579  isass  33625  isexid  33626  ismndo2  33653  exidreslem  33656  rngodm1dm2  33711  divrngcl  33736  isdrngo2  33737  isopos  34293  isatl  34412  dibffval  36255  dibfval  36256  conrel2d  37782  iunrelexp0  37820  dmtrclfvRP  37848  rntrclfvRP  37849  neicvgbex  38236  dvsconst  38355  expgrowth  38360  fnlimfvre  39712  dvsinax  39896  dvmptresicc  39903  dvcosax  39910  dvbdfbdioolem1  39912  itgsinexplem1  39938  itgcoscmulx  39954  dirkeritg  40088  dirkercncflem2  40090  fourierdlem60  40152  fourierdlem61  40153  fourierdlem74  40166  fourierdlem75  40167  fourierdlem80  40172  fourierdlem94  40186  fourierdlem103  40195  fourierdlem104  40196  fourierdlem113  40205  dmvon  40589  ovnovollem1  40639  smflimlem3  40750  smflimlem4  40751  smflim  40754  smflim2  40781  smfpimcc  40783  smflimmpt  40785  smfsuplem2  40787  smfsuplem3  40788  smfsup  40789  smfsupmpt  40790  smfinflem  40792  smfinf  40793  smfinfmpt  40794  smflimsuplem1  40795  smflimsuplem2  40796  smflimsuplem3  40797  smflimsuplem4  40798  smflimsuplem7  40801  smflimsup  40803  smflimsupmpt  40804  smfliminf  40806  smfliminfmpt  40807  dfateq12d  40978  upwlksfval  41487  mndpsuppss  41923
  Copyright terms: Public domain W3C validator