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

Theorem dmeqd 5064
Description: Equality deduction for domain. (Contributed by NM, 4-Mar-2004.)
Hypothesis
Ref Expression
dmeqd.1  |-  ( ph  ->  A  =  B )
Assertion
Ref Expression
dmeqd  |-  ( ph  ->  dom  A  =  dom  B )

Proof of Theorem dmeqd
StepHypRef Expression
1 dmeqd.1 . 2  |-  ( ph  ->  A  =  B )
2 dmeq 5062 . 2  |-  ( A  =  B  ->  dom  A  =  dom  B )
31, 2syl 16 1  |-  ( ph  ->  dom  A  =  dom  B )
Colors of variables: wff set class
Syntax hints:    -> wi 4    = wceq 1652   dom cdm 4870
This theorem is referenced by:  dmxpid  5081  rneq  5087  dmxpss  5292  dmsnopss  5334  dmsnsnsn  5340  elxp4  5349  fndmin  5829  1stval  6343  fo1st  6358  f1stres  6360  bropopvvv  6418  errn  6919  xpassen  7194  xpdom2  7195  oicl  7490  oif  7491  hartogslem1  7503  cantnfdm  7611  cantnfval  7615  cantnf0  7622  cantnfres  7625  cnfcomlem  7648  hsmexlem4  8301  hsmexlem5  8302  axdc3lem2  8323  ttukeylem3  8383  hashfun  11692  swrdval  11756  s4dom  11858  shftdm  11878  rlim  12281  ramval  13368  isstruct2  13470  setsvalg  13484  prdsval  13670  homfeqbas  13914  invf  13985  oppciso  13994  sscfn1  14009  sscfn2  14010  isssc  14012  rescval  14019  rescval2  14020  issubc  14027  issubc2  14028  cofuval  14071  resfval  14081  resfval2  14082  resf1st  14083  prfval  14288  gsumvalx  14766  cntzrcl  15118  dmdprd  15551  dprdval  15553  dpjfval  15605  ablfaclem3  15637  elocv  16887  ishil  16937  iscnp2  17295  ptval  17594  ptcmplem2  18076  cnextfval  18085  tsmsval2  18151  ustbas2  18247  utopval  18254  tusval  18288  ucnval  18299  iscfilu  18310  psmetdmdm  18328  xmetdmdm  18357  blfvalps  18405  setsmstopn  18500  tmsval  18503  metuvalOLD  18571  metuval  18572  tngtopn  18683  cfilfval  19209  caufval  19220  limcfval  19751  dvfval  19776  dvbsss  19781  perfdvf  19782  dvn2bss  19808  dvnres  19809  dvcmul  19822  dvcmulf  19823  dvcj  19828  dvnfre  19830  dvexp  19831  dvmptres3  19834  dvmptcl  19837  dvmptadd  19838  dvmptmul  19839  dvmptres2  19840  dvmptcmul  19842  dvmptcj  19846  dvmptco  19850  rolle  19866  cmvth  19867  mvth  19868  dvlip  19869  dvlipcn  19870  dvlip2  19871  c1liplem1  19872  dveq0  19876  dv11cn  19877  dvle  19883  dvivthlem1  19884  dvivth  19886  dvne0  19887  lhop1lem  19889  lhop2  19891  lhop  19892  dvcnvrelem1  19893  dvcvx  19896  dvfsumle  19897  dvfsumge  19898  dvfsumabs  19899  dvmptrecl  19900  dvfsumlem2  19903  itgsubstlem  19924  mpfrcl  19931  taylfval  20267  tayl0  20270  dvtaylp  20278  dvntaylp  20279  dvntaylp0  20280  taylthlem1  20281  taylthlem2  20282  ulmdvlem1  20308  pserdv  20337  pige3  20417  logtayl  20543  isumgra  21342  vdgrfval  21658  iseupa  21679  grporndm  21790  isabloda  21879  isass  21896  isexid  21897  ismndo2  21925  rngodm1dm2  21998  vcoprne  22050  hmoval  22303  metidval  24277  pstmval  24282  ofcfval  24473  ofcfval3  24477  brae  24584  braew  24585  faeval  24589  mbfmcst  24601  issibf  24640  sitmval  24653  0rrv  24701  dstrvprob  24721  lgamgulmlem2  24806  relexpdm  25127  areacirclem3  26283  sdclem2  26437  ismtyval  26500  exidreslem  26543  divrngcl  26564  isdrngo2  26565  fninfp  26726  fndifnfp  26728  dsmmval  27168  f1omvdco2  27359  pmtrfrn  27368  symgsssg  27376  symgfisg  27377  symggen  27379  psgnunilem1  27384  psgnunilem5  27385  psgnunilem2  27386  psgnunilem3  27387  psgneldm  27394  dvsconst  27515  expgrowth  27520  itgsinexplem1  27715  dfateq12d  27960  2wlkonot3v  28295  2spthonot3v  28296  dibffval  31875  dibfval  31876
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1555  ax-5 1566  ax-17 1626  ax-9 1666  ax-8 1687  ax-6 1744  ax-7 1749  ax-11 1761  ax-12 1950  ax-ext 2416
This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-3an 938  df-tru 1328  df-ex 1551  df-nf 1554  df-sb 1659  df-clab 2422  df-cleq 2428  df-clel 2431  df-nfc 2560  df-rab 2706  df-v 2950  df-dif 3315  df-un 3317  df-in 3319  df-ss 3326  df-nul 3621  df-if 3732  df-sn 3812  df-pr 3813  df-op 3815  df-br 4205  df-dm 4880
  Copyright terms: Public domain W3C validator