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

Theorem dmeqi 5037
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 5036 . 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 1364   dom cdm 4836
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1596  ax-4 1607  ax-5 1675  ax-6 1713  ax-7 1733  ax-10 1780  ax-11 1785  ax-12 1797  ax-13 1948  ax-ext 2422
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 962  df-tru 1367  df-ex 1592  df-nf 1595  df-sb 1706  df-clab 2428  df-cleq 2434  df-clel 2437  df-nfc 2566  df-rab 2722  df-v 2972  df-dif 3328  df-un 3330  df-in 3332  df-ss 3339  df-nul 3635  df-if 3789  df-sn 3875  df-pr 3877  df-op 3881  df-br 4290  df-dm 4846
This theorem is referenced by:  dmxp  5054  dmxpin  5056  rncoss  5096  rncoeq  5099  rnun  5242  rnin  5243  rnxp  5265  rnxpss  5267  imainrect  5276  dmpropg  5309  dmtpop  5312  rnsnopg  5315  fntpg  5470  opabiotadm  5750  dffv2  5761  fvopab4ndm  5791  fnreseql  5810  dmoprab  6170  reldmmpt2  6200  elmpt2cl  6303  bropopvvv  6652  mpt2ndm0  6738  tfrlem8  6839  tfr1a  6849  tfr2a  6850  tfr2b  6851  rdgseg  6874  xpassen  7401  sbthlem5  7421  hartogslem1  7752  r1funlim  7969  r1sucg  7972  r1limg  7974  rankf  7997  hsmexlem4  8594  axdc2lem  8613  dmaddpi  9055  dmmulpi  9056  dmaddsr  9248  dmmulsr  9249  axaddf  9308  axmulf  9309  strlemor1  14261  divsfval  14481  xpsfrnel2  14499  mvdco  15944  symgsssg  15966  symgfisg  15967  pmtrdifellem2  15976  psgnunilem5  15993  ismbl  20968  volres  20970  efcvx  21873  dvrelog  22041  dvlog  22055  usgrares1  23258  usgrafilem1  23259  cusgrasizeindslem2  23317  wlkntrllem1  23393  eupares  23531  resgrprn  23702  ismgm  23742  dfhnorm2  24459  hlimcaui  24574  hhshsslem1  24603  dmadjss  25226  adjeu  25228  adj1o  25233  gsummpt2co  26184  prsdm  26280  mbfmcst  26610  eulerpartlemt  26684  0rrv  26764  coinflipspace  26793  ghomfo  27239  wfrlem7  27659  wfrlem9  27661  wfrlem16  27668  frrlem7  27707  nofulllem5  27776  fixun  27869  linedegen  28103  ssbnd  28612  exidreslem  28667  dmmzp  28994  dvsid  29530  dvsef  29531  stoweidlem27  29747  2wlkonot3v  30319  2spthonot3v  30320  clwwlknprop  30360  bnj96  31692  bnj1398  31859  bnj1416  31864  bnj1450  31875  bnj1498  31886  bnj1501  31892
  Copyright terms: Public domain W3C validator