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

Theorem dmeqi 5056
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 5055 . 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 1369   dom cdm 4855
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-10 1775  ax-11 1780  ax-12 1792  ax-13 1943  ax-ext 2423
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 967  df-tru 1372  df-ex 1587  df-nf 1590  df-sb 1701  df-clab 2430  df-cleq 2436  df-clel 2439  df-nfc 2577  df-rab 2739  df-v 2989  df-dif 3346  df-un 3348  df-in 3350  df-ss 3357  df-nul 3653  df-if 3807  df-sn 3893  df-pr 3895  df-op 3899  df-br 4308  df-dm 4865
This theorem is referenced by:  dmxp  5073  dmxpin  5075  rncoss  5115  rncoeq  5118  rnun  5260  rnin  5261  rnxp  5283  rnxpss  5285  imainrect  5294  dmpropg  5327  dmtpop  5330  rnsnopg  5333  fntpg  5488  opabiotadm  5768  dffv2  5779  fvopab4ndm  5809  fnreseql  5828  dmoprab  6186  reldmmpt2  6216  elmpt2cl  6319  bropopvvv  6668  mpt2ndm0  6754  tfrlem8  6858  tfr1a  6868  tfr2a  6869  tfr2b  6870  rdgseg  6893  xpassen  7420  sbthlem5  7440  hartogslem1  7771  r1funlim  7988  r1sucg  7991  r1limg  7993  rankf  8016  hsmexlem4  8613  axdc2lem  8632  dmaddpi  9074  dmmulpi  9075  dmaddsr  9267  dmmulsr  9268  axaddf  9327  axmulf  9328  strlemor1  14280  divsfval  14500  xpsfrnel2  14518  mvdco  15966  symgsssg  15988  symgfisg  15989  pmtrdifellem2  15998  psgnunilem5  16015  ismbl  21024  volres  21026  efcvx  21929  dvrelog  22097  dvlog  22111  usgrares1  23338  usgrafilem1  23339  cusgrasizeindslem2  23397  wlkntrllem1  23473  eupares  23611  resgrprn  23782  ismgm  23822  dfhnorm2  24539  hlimcaui  24654  hhshsslem1  24683  dmadjss  25306  adjeu  25308  adj1o  25313  gsummpt2co  26264  prsdm  26359  mbfmcst  26689  eulerpartlemt  26769  0rrv  26849  coinflipspace  26878  ghomfo  27325  wfrlem7  27745  wfrlem9  27747  wfrlem16  27754  frrlem7  27793  nofulllem5  27862  fixun  27955  linedegen  28189  ssbnd  28706  exidreslem  28761  dmmzp  29088  dvsid  29624  dvsef  29625  stoweidlem27  29841  2wlkonot3v  30413  2spthonot3v  30414  clwwlknprop  30454  bnj96  31877  bnj1398  32044  bnj1416  32049  bnj1450  32060  bnj1498  32071  bnj1501  32077
  Copyright terms: Public domain W3C validator