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 1437   dom cdm 4854
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1665  ax-4 1678  ax-5 1751  ax-6 1797  ax-7 1841  ax-10 1889  ax-11 1894  ax-12 1907  ax-13 2055  ax-ext 2407
This theorem depends on definitions:  df-bi 188  df-or 371  df-an 372  df-3an 984  df-tru 1440  df-ex 1660  df-nf 1664  df-sb 1790  df-clab 2415  df-cleq 2421  df-clel 2424  df-nfc 2579  df-rab 2791  df-v 3089  df-dif 3445  df-un 3447  df-in 3449  df-ss 3456  df-nul 3768  df-if 3916  df-sn 4003  df-pr 4005  df-op 4009  df-br 4427  df-dm 4864
This theorem is referenced by:  dmxp  5073  dmxpin  5075  rncoss  5115  rncoeq  5118  rnun  5264  rnin  5265  rnxp  5287  rnxpss  5289  imainrect  5298  dmpropg  5329  dmtpop  5332  rnsnopg  5335  fntpg  5656  opabiotadm  5943  dffv2  5954  fvopab4ndm  5988  fnreseql  6007  dmoprab  6391  reldmmpt2  6421  mpt2ndm0  6524  elmpt2cl  6525  bropopvvv  6887  wfrdmss  7050  wfrdmcl  7052  wfrlem16  7059  tfrlem8  7110  tfr1a  7120  tfr2a  7121  tfr2b  7122  rdgseg  7148  xpassen  7672  sbthlem5  7692  hartogslem1  8057  r1funlim  8236  r1sucg  8239  r1limg  8241  rankf  8264  hsmexlem4  8857  axdc2lem  8876  dmaddpi  9314  dmmulpi  9315  dmaddsr  9508  dmmulsr  9509  axaddf  9568  axmulf  9569  strlemor1  15179  divsfval  15404  xpsfrnel2  15422  mvdco  17037  symgsssg  17059  symgfisg  17060  pmtrdifellem2  17069  psgnunilem5  17086  ismbl  22357  volres  22359  efcvx  23269  dvrelog  23447  dvlog  23461  usgrares1  24983  usgrafilem1  24984  cusgrasizeindslem2  25047  wlkntrllem1  25134  clwwlknprop  25345  2wlkonot3v  25448  2spthonot3v  25449  eupares  25548  resgrprn  25853  ismgmOLD  25893  dfhnorm2  26610  hlimcaui  26724  hhshsslem1  26753  dmadjss  27375  adjeu  27377  adj1o  27382  gsummpt2co  28381  prsdm  28559  mbfmcst  28920  eulerpartlemt  29030  0rrv  29110  coinflipspace  29139  bnj96  29464  bnj1398  29631  bnj1416  29636  bnj1450  29647  bnj1498  29658  bnj1501  29664  ghomfo  30097  frrlem7  30311  nofulllem5  30380  fixun  30461  linedegen  30695  ssbnd  31824  exidreslem  31879  dmmzp  35284  dvsid  36317  dvsef  36318  dvsinax  37355  fperdvper  37362  dvcosax  37370  stoweidlem27  37456  fourierdlem57  37595  fourierdlem58  37596  fourierdlem62  37600  fourierdlem80  37618  fourierdlem94  37632  fourierdlem97  37635  fourierdlem113  37651  fouriersw  37663  fouriercn  37664  isuhgr  38436  isushgr  38437  elbigofrcl  39122
  Copyright terms: Public domain W3C validator