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

Theorem dmeqi 5117
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 5116 . 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 1399   dom cdm 4913
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1626  ax-4 1639  ax-5 1712  ax-6 1755  ax-7 1798  ax-10 1845  ax-11 1850  ax-12 1862  ax-13 2006  ax-ext 2360
This theorem depends on definitions:  df-bi 185  df-or 368  df-an 369  df-3an 973  df-tru 1402  df-ex 1621  df-nf 1625  df-sb 1748  df-clab 2368  df-cleq 2374  df-clel 2377  df-nfc 2532  df-rab 2741  df-v 3036  df-dif 3392  df-un 3394  df-in 3396  df-ss 3403  df-nul 3712  df-if 3858  df-sn 3945  df-pr 3947  df-op 3951  df-br 4368  df-dm 4923
This theorem is referenced by:  dmxp  5134  dmxpin  5136  rncoss  5176  rncoeq  5179  rnun  5324  rnin  5325  rnxp  5347  rnxpss  5349  imainrect  5358  dmpropg  5389  dmtpop  5392  rnsnopg  5395  fntpg  5551  opabiotadm  5836  dffv2  5847  fvopab4ndm  5880  fnreseql  5899  dmoprab  6282  reldmmpt2  6312  mpt2ndm0  6415  elmpt2cl  6416  bropopvvv  6779  tfrlem8  6971  tfr1a  6981  tfr2a  6982  tfr2b  6983  rdgseg  7006  xpassen  7530  sbthlem5  7550  hartogslem1  7882  r1funlim  8097  r1sucg  8100  r1limg  8102  rankf  8125  hsmexlem4  8722  axdc2lem  8741  dmaddpi  9179  dmmulpi  9180  dmaddsr  9373  dmmulsr  9374  axaddf  9433  axmulf  9434  strlemor1  14729  divsfval  14954  xpsfrnel2  14972  mvdco  16587  symgsssg  16609  symgfisg  16610  pmtrdifellem2  16619  psgnunilem5  16636  ismbl  22022  volres  22024  efcvx  22929  dvrelog  23105  dvlog  23119  usgrares1  24531  usgrafilem1  24532  cusgrasizeindslem2  24595  wlkntrllem1  24682  clwwlknprop  24893  2wlkonot3v  24996  2spthonot3v  24997  eupares  25096  resgrprn  25399  ismgmOLD  25439  dfhnorm2  26156  hlimcaui  26271  hhshsslem1  26300  dmadjss  26922  adjeu  26924  adj1o  26929  gsummpt2co  27924  prsdm  28050  mbfmcst  28386  eulerpartlemt  28493  0rrv  28573  coinflipspace  28602  ghomfo  29220  wfrlem7  29514  wfrlem9  29516  wfrlem16  29523  frrlem7  29562  nofulllem5  29631  fixun  29712  linedegen  29946  ssbnd  30450  exidreslem  30505  dmmzp  30831  dvsid  31404  dvsef  31405  dvsinax  31874  fperdvper  31881  dvcosax  31889  stoweidlem27  31975  fourierdlem57  32112  fourierdlem58  32113  fourierdlem62  32117  fourierdlem80  32135  fourierdlem94  32149  fourierdlem97  32152  fourierdlem113  32168  fouriersw  32180  fouriercn  32181  isuhgr  32684  isushgr  32685  elbigofrcl  33371  bnj96  34270  bnj1398  34437  bnj1416  34442  bnj1450  34453  bnj1498  34464  bnj1501  34470
  Copyright terms: Public domain W3C validator