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

Theorem dmeqi 5055
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 5054 . 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 1437   dom cdm 4853
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1663  ax-4 1676  ax-5 1752  ax-6 1798  ax-7 1843  ax-10 1891  ax-11 1896  ax-12 1909  ax-13 2057  ax-ext 2401
This theorem depends on definitions:  df-bi 188  df-or 371  df-an 372  df-3an 984  df-tru 1440  df-ex 1658  df-nf 1662  df-sb 1791  df-clab 2408  df-cleq 2414  df-clel 2417  df-nfc 2568  df-rab 2780  df-v 3082  df-dif 3439  df-un 3441  df-in 3443  df-ss 3450  df-nul 3762  df-if 3912  df-sn 3999  df-pr 4001  df-op 4005  df-br 4424  df-dm 4863
This theorem is referenced by:  dmxp  5072  dmxpin  5074  rncoss  5114  rncoeq  5117  rnun  5263  rnin  5264  rnxp  5286  rnxpss  5288  imainrect  5297  dmpropg  5328  dmtpop  5331  rnsnopg  5334  fntpg  5656  opabiotadm  5944  dffv2  5955  fvopab4ndm  5989  fnreseql  6008  dmoprab  6392  reldmmpt2  6422  mpt2ndm0  6525  elmpt2cl  6526  bropopvvv  6888  wfrdmss  7054  wfrdmcl  7056  wfrlem16  7063  tfrlem8  7114  tfr1a  7124  tfr2a  7125  tfr2b  7126  rdgseg  7152  xpassen  7676  sbthlem5  7696  hartogslem1  8067  r1funlim  8246  r1sucg  8249  r1limg  8251  rankf  8274  hsmexlem4  8867  axdc2lem  8886  dmaddpi  9323  dmmulpi  9324  dmaddsr  9517  dmmulsr  9518  axaddf  9577  axmulf  9578  strlemor1  15217  divsfval  15453  xpsfrnel2  15471  mvdco  17086  symgsssg  17108  symgfisg  17109  pmtrdifellem2  17118  psgnunilem5  17135  ismbl  22479  volres  22481  efcvx  23403  dvrelog  23581  dvlog  23595  usgrares1  25137  usgrafilem1  25138  cusgrasizeindslem2  25201  wlkntrllem1  25288  clwwlknprop  25499  2wlkonot3v  25602  2spthonot3v  25603  eupares  25702  resgrprn  26007  ismgmOLD  26047  dfhnorm2  26774  hlimcaui  26888  hhshsslem1  26917  dmadjss  27539  adjeu  27541  adj1o  27546  gsummpt2co  28551  prsdm  28729  mbfmcst  29090  eulerpartlemt  29213  0rrv  29293  coinflipspace  29322  bnj96  29685  bnj1398  29852  bnj1416  29857  bnj1450  29868  bnj1498  29879  bnj1501  29885  ghomfo  30318  frrlem7  30532  nofulllem5  30601  fixun  30682  linedegen  30916  ssbnd  32085  exidreslem  32140  dmmzp  35545  cnvrcl0  36203  dvsid  36651  dvsef  36652  dvsinax  37724  fperdvper  37731  dvcosax  37739  stoweidlem27  37828  fourierdlem57  37968  fourierdlem58  37969  fourierdlem62  37973  fourierdlem80  37991  fourierdlem94  38005  fourierdlem97  38008  fourierdlem113  38024  fouriersw  38036  fouriercn  38037  0ome  38259  structiedg0val  38956  snstriedgval  38970  isuhgr  38983  isushgr  38984  isupgr  39008  isumgr  39017  isuspgr  39056  isusgr  39057  usgredgedga  39112  issubgr  39138  subgruhgredgd  39151  subumgredg2  39152  isuhgrALTV  39327  isushgrALTV  39328  elbigofrcl  40012
  Copyright terms: Public domain W3C validator