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

Theorem dmeqi 4896
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 4895 . 2  |-  ( A  =  B  ->  dom  A  =  dom  B )
31, 2ax-mp 8 1  |-  dom  A  =  dom  B
Colors of variables: wff set class
Syntax hints:    = wceq 1632   dom cdm 4705
This theorem is referenced by:  dmxp  4913  dmxpin  4915  rncoss  4961  rncoeq  4964  rnun  5105  rnin  5106  rnxp  5122  rnxpss  5124  imainrect  5135  dmpropg  5162  dmtpop  5165  rnsnopg  5168  dffv2  5608  fvopab4ndm  5636  fnreseql  5651  dmoprab  5944  reldmmpt2  5971  elmpt2cl  6077  opabiotadm  6308  tfrlem8  6416  tfr1a  6426  tfr2a  6427  tfr2b  6428  rdgseg  6451  xpassen  6972  sbthlem5  6991  hartogslem1  7273  r1funlim  7454  r1sucg  7457  r1limg  7459  rankf  7482  hsmexlem4  8071  axdc2lem  8090  dmaddpi  8530  dmmulpi  8531  dmaddsr  8723  dmmulsr  8724  axaddf  8783  axmulf  8784  strlemor1  13251  divsfval  13465  xpsfrnel2  13483  ismbl  18901  volres  18903  efcvx  19841  dvrelog  20000  dvlog  20014  resgrprn  20963  ismgm  21003  dfhnorm2  21717  hlimcaui  21832  hhshsslem1  21860  dmadjss  22483  adjeu  22485  adj1o  22490  xppreima2  23227  mbfmcst  23579  0rrv  23669  coinflipspace  23696  eupares  23914  ghomfo  24013  wfrlem7  24333  wfrlem9  24335  wfrlem16  24342  frrlem7  24362  nofulllem5  24431  fixun  24520  linedegen  24838  dmoprabsss  25136  nZdef  25283  inpc  25380  dominc  25383  domncnt  25385  ranncnt  25386  aidm2  25853  dmrngcmp  25854  dmo  25879  jdmo  25881  cmpmorp  25882  mrdmcd  25897  homib  25899  cmphmia  25901  cmphmib  25902  iri  25903  idmon  25920  idsubidsup  25960  prismorcsetlemc  26020  domdomcatfun1  26030  pgapspf2  26156  ssbnd  26615  exidreslem  26670  dmmzp  26914  mvdco  27491  symgsssg  27511  symgfisg  27512  psgnunilem5  27520  dvsid  27651  dvsef  27652  mpt2ndm0  28204  trlonprop  28341  wlkntrllem1  28345  bnj96  29213  bnj1398  29380  bnj1416  29385  bnj1450  29396  bnj1498  29407  bnj1501  29413
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1536  ax-5 1547  ax-17 1606  ax-9 1644  ax-8 1661  ax-6 1715  ax-7 1720  ax-11 1727  ax-12 1878  ax-ext 2277
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-3an 936  df-tru 1310  df-ex 1532  df-nf 1535  df-sb 1639  df-clab 2283  df-cleq 2289  df-clel 2292  df-nfc 2421  df-rab 2565  df-v 2803  df-dif 3168  df-un 3170  df-in 3172  df-ss 3179  df-nul 3469  df-if 3579  df-sn 3659  df-pr 3660  df-op 3662  df-br 4040  df-dm 4715
  Copyright terms: Public domain W3C validator