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

Theorem dmeqi 5202
Description: Equality inference for domain. (Contributed by NM, 4-Mar-2004.)
Hypothesis
Ref Expression
dmeqi.1  |-  A  =  B
Assertion
Ref Expression
dmeqi  |-  dom  A  =  dom  B

Proof of Theorem dmeqi
StepHypRef Expression
1 dmeqi.1 . 2  |-  A  =  B
2 dmeq 5201 . 2  |-  ( A  =  B  ->  dom  A  =  dom  B )
31, 2ax-mp 5 1  |-  dom  A  =  dom  B
Colors of variables: wff setvar class
Syntax hints:    = wceq 1379   dom cdm 4999
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1601  ax-4 1612  ax-5 1680  ax-6 1719  ax-7 1739  ax-10 1786  ax-11 1791  ax-12 1803  ax-13 1968  ax-ext 2445
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 975  df-tru 1382  df-ex 1597  df-nf 1600  df-sb 1712  df-clab 2453  df-cleq 2459  df-clel 2462  df-nfc 2617  df-rab 2823  df-v 3115  df-dif 3479  df-un 3481  df-in 3483  df-ss 3490  df-nul 3786  df-if 3940  df-sn 4028  df-pr 4030  df-op 4034  df-br 4448  df-dm 5009
This theorem is referenced by:  dmxp  5219  dmxpin  5221  rncoss  5261  rncoeq  5264  rnun  5412  rnin  5413  rnxp  5435  rnxpss  5437  imainrect  5446  dmpropg  5479  dmtpop  5482  rnsnopg  5485  fntpg  5641  opabiotadm  5927  dffv2  5938  fvopab4ndm  5970  fnreseql  5989  dmoprab  6365  reldmmpt2  6395  mpt2ndm0  6498  elmpt2cl  6499  bropopvvv  6860  tfrlem8  7050  tfr1a  7060  tfr2a  7061  tfr2b  7062  rdgseg  7085  xpassen  7608  sbthlem5  7628  hartogslem1  7963  r1funlim  8180  r1sucg  8183  r1limg  8185  rankf  8208  hsmexlem4  8805  axdc2lem  8824  dmaddpi  9264  dmmulpi  9265  dmaddsr  9458  dmmulsr  9459  axaddf  9518  axmulf  9519  strlemor1  14578  divsfval  14798  xpsfrnel2  14816  mvdco  16266  symgsssg  16288  symgfisg  16289  pmtrdifellem2  16298  psgnunilem5  16315  ismbl  21672  volres  21674  efcvx  22578  dvrelog  22746  dvlog  22760  usgrares1  24086  usgrafilem1  24087  cusgrasizeindslem2  24150  wlkntrllem1  24237  clwwlknprop  24448  2wlkonot3v  24551  2spthonot3v  24552  eupares  24651  resgrprn  24958  ismgm  24998  dfhnorm2  25715  hlimcaui  25830  hhshsslem1  25859  dmadjss  26482  adjeu  26484  adj1o  26489  gsummpt2co  27434  prsdm  27532  mbfmcst  27870  eulerpartlemt  27950  0rrv  28030  coinflipspace  28059  ghomfo  28506  wfrlem7  28926  wfrlem9  28928  wfrlem16  28935  frrlem7  28974  nofulllem5  29043  fixun  29136  linedegen  29370  ssbnd  29887  exidreslem  29942  dmmzp  30269  dvsid  30836  dvsef  30837  dvsinax  31241  fperdvper  31248  dvcosax  31256  stoweidlem27  31327  fourierdlem57  31464  fourierdlem58  31465  fourierdlem62  31469  fourierdlem70  31477  fourierdlem71  31478  fourierdlem80  31487  fourierdlem94  31501  fourierdlem97  31504  fourierdlem113  31520  fouriersw  31532  fouriercn  31533  isuhgr  31835  isushgr  31836  bnj96  33002  bnj1398  33169  bnj1416  33174  bnj1450  33185  bnj1498  33196  bnj1501  33202
  Copyright terms: Public domain W3C validator