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

Theorem dmeqi 5071
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 5070 . 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 1652   dom cdm 4878
This theorem is referenced by:  dmxp  5088  dmxpin  5090  rncoss  5136  rncoeq  5139  rnun  5280  rnin  5281  rnxp  5299  rnxpss  5301  imainrect  5312  dmpropg  5343  dmtpop  5346  rnsnopg  5349  fntpg  5506  dffv2  5796  fvopab4ndm  5825  fnreseql  5840  dmoprab  6154  reldmmpt2  6181  elmpt2cl  6288  bropopvvv  6426  mpt2ndm0  6473  opabiotadm  6537  tfrlem8  6645  tfr1a  6655  tfr2a  6656  tfr2b  6657  rdgseg  6680  xpassen  7202  sbthlem5  7221  hartogslem1  7511  r1funlim  7692  r1sucg  7695  r1limg  7697  rankf  7720  hsmexlem4  8309  axdc2lem  8328  dmaddpi  8767  dmmulpi  8768  dmaddsr  8960  dmmulsr  8961  axaddf  9020  axmulf  9021  strlemor1  13556  divsfval  13772  xpsfrnel2  13790  ismbl  19422  volres  19424  efcvx  20365  dvrelog  20528  dvlog  20542  usgrares1  21424  usgrafilem1  21425  cusgrasizeindslem2  21483  wlkntrllem1  21559  eupares  21697  resgrprn  21868  ismgm  21908  dfhnorm2  22624  hlimcaui  22739  hhshsslem1  22767  dmadjss  23390  adjeu  23392  adj1o  23397  mbfmcst  24609  0rrv  24709  coinflipspace  24738  ghomfo  25102  wfrlem7  25544  wfrlem9  25546  wfrlem16  25553  frrlem7  25592  nofulllem5  25661  fixun  25754  linedegen  26077  ssbnd  26497  exidreslem  26552  dmmzp  26790  mvdco  27365  symgsssg  27385  symgfisg  27386  psgnunilem5  27394  dvsid  27525  dvsef  27526  stoweidlem27  27752  2wlkonot3v  28342  2spthonot3v  28343  bnj96  29236  bnj1398  29403  bnj1416  29408  bnj1450  29419  bnj1498  29430  bnj1501  29436
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 2417
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 2423  df-cleq 2429  df-clel 2432  df-nfc 2561  df-rab 2714  df-v 2958  df-dif 3323  df-un 3325  df-in 3327  df-ss 3334  df-nul 3629  df-if 3740  df-sn 3820  df-pr 3821  df-op 3823  df-br 4213  df-dm 4888
  Copyright terms: Public domain W3C validator