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

Theorem dmeqi 5194
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 5193 . 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 1383   dom cdm 4989
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1605  ax-4 1618  ax-5 1691  ax-6 1734  ax-7 1776  ax-10 1823  ax-11 1828  ax-12 1840  ax-13 1985  ax-ext 2421
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 976  df-tru 1386  df-ex 1600  df-nf 1604  df-sb 1727  df-clab 2429  df-cleq 2435  df-clel 2438  df-nfc 2593  df-rab 2802  df-v 3097  df-dif 3464  df-un 3466  df-in 3468  df-ss 3475  df-nul 3771  df-if 3927  df-sn 4015  df-pr 4017  df-op 4021  df-br 4438  df-dm 4999
This theorem is referenced by:  dmxp  5211  dmxpin  5213  rncoss  5253  rncoeq  5256  rnun  5404  rnin  5405  rnxp  5427  rnxpss  5429  imainrect  5438  dmpropg  5471  dmtpop  5474  rnsnopg  5477  fntpg  5633  opabiotadm  5920  dffv2  5931  fvopab4ndm  5963  fnreseql  5982  dmoprab  6368  reldmmpt2  6398  mpt2ndm0  6501  elmpt2cl  6502  bropopvvv  6865  tfrlem8  7055  tfr1a  7065  tfr2a  7066  tfr2b  7067  rdgseg  7090  xpassen  7613  sbthlem5  7633  hartogslem1  7970  r1funlim  8187  r1sucg  8190  r1limg  8192  rankf  8215  hsmexlem4  8812  axdc2lem  8831  dmaddpi  9271  dmmulpi  9272  dmaddsr  9465  dmmulsr  9466  axaddf  9525  axmulf  9526  strlemor1  14706  divsfval  14926  xpsfrnel2  14944  mvdco  16449  symgsssg  16471  symgfisg  16472  pmtrdifellem2  16481  psgnunilem5  16498  ismbl  21915  volres  21917  efcvx  22822  dvrelog  22996  dvlog  23010  usgrares1  24388  usgrafilem1  24389  cusgrasizeindslem2  24452  wlkntrllem1  24539  clwwlknprop  24750  2wlkonot3v  24853  2spthonot3v  24854  eupares  24953  resgrprn  25260  ismgmOLD  25300  dfhnorm2  26017  hlimcaui  26132  hhshsslem1  26161  dmadjss  26784  adjeu  26786  adj1o  26791  prsdm  27874  mbfmcst  28208  eulerpartlemt  28288  0rrv  28368  coinflipspace  28397  ghomfo  29009  wfrlem7  29325  wfrlem9  29327  wfrlem16  29334  frrlem7  29373  nofulllem5  29442  fixun  29535  linedegen  29769  ssbnd  30260  exidreslem  30315  dmmzp  30641  dvsid  31212  dvsef  31213  dvsinax  31662  fperdvper  31669  dvcosax  31677  stoweidlem27  31763  fourierdlem57  31900  fourierdlem58  31901  fourierdlem62  31905  fourierdlem80  31923  fourierdlem94  31937  fourierdlem97  31940  fourierdlem113  31956  fouriersw  31968  fouriercn  31969  isuhgr  32320  isushgr  32321  bnj96  33791  bnj1398  33958  bnj1416  33963  bnj1450  33974  bnj1498  33985  bnj1501  33991
  Copyright terms: Public domain W3C validator