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

Theorem dmeqi 5058
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 5057 . 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 1455   dom cdm 4856
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1680  ax-4 1693  ax-5 1769  ax-6 1816  ax-7 1862  ax-10 1926  ax-11 1931  ax-12 1944  ax-13 2102  ax-ext 2442
This theorem depends on definitions:  df-bi 190  df-or 376  df-an 377  df-3an 993  df-tru 1458  df-ex 1675  df-nf 1679  df-sb 1809  df-clab 2449  df-cleq 2455  df-clel 2458  df-nfc 2592  df-rab 2758  df-v 3059  df-dif 3419  df-un 3421  df-in 3423  df-ss 3430  df-nul 3744  df-if 3894  df-sn 3981  df-pr 3983  df-op 3987  df-br 4419  df-dm 4866
This theorem is referenced by:  dmxp  5075  dmxpin  5077  rncoss  5117  rncoeq  5120  rnun  5266  rnin  5267  rnxp  5289  rnxpss  5291  imainrect  5300  dmpropg  5332  dmtpop  5335  rnsnopg  5338  fntpg  5660  opabiotadm  5955  dffv2  5966  fvopab4ndm  6000  fnreseql  6020  dmoprab  6409  reldmmpt2  6439  mpt2ndm0  6542  elmpt2cl  6543  bropopvvv  6906  bropfvvvv  6908  wfrdmss  7073  wfrdmcl  7075  wfrlem16  7082  tfrlem8  7133  tfr1a  7143  tfr2a  7144  tfr2b  7145  rdgseg  7171  xpassen  7697  sbthlem5  7717  hartogslem1  8088  r1funlim  8268  r1sucg  8271  r1limg  8273  rankf  8296  hsmexlem4  8890  axdc2lem  8909  dmaddpi  9346  dmmulpi  9347  dmaddsr  9540  dmmulsr  9541  axaddf  9600  axmulf  9601  strlemor1  15272  divsfval  15508  xpsfrnel2  15526  mvdco  17141  symgsssg  17163  symgfisg  17164  pmtrdifellem2  17173  psgnunilem5  17190  ismbl  22535  volres  22537  efcvx  23460  dvrelog  23638  dvlog  23652  usgrares1  25194  usgrafilem1  25195  cusgrasizeindslem2  25258  wlkntrllem1  25345  clwwlknprop  25556  2wlkonot3v  25659  2spthonot3v  25660  eupares  25759  resgrprn  26064  ismgmOLD  26104  dfhnorm2  26831  hlimcaui  26945  hhshsslem1  26974  dmadjss  27596  adjeu  27598  adj1o  27603  gsummpt2co  28594  prsdm  28771  mbfmcst  29131  eulerpartlemt  29254  0rrv  29334  coinflipspace  29363  bnj96  29726  bnj1398  29893  bnj1416  29898  bnj1450  29909  bnj1498  29920  bnj1501  29926  ghomfo  30359  frrlem7  30574  nofulllem5  30645  fixun  30726  linedegen  30960  ssbnd  32166  exidreslem  32221  dmmzp  35621  cnvrcl0  36278  dvsid  36725  dvsef  36726  dvsinax  37869  fperdvper  37876  dvcosax  37884  stoweidlem27  37988  fourierdlem57  38128  fourierdlem58  38129  fourierdlem62  38133  fourierdlem80  38151  fourierdlem94  38165  fourierdlem97  38168  fourierdlem113  38184  fouriersw  38196  fouriercn  38197  0ome  38458  hoi2toco  38536  opabn1stprc  39143  structiedg0val  39266  snstriedgval  39280  isuhgr  39293  isushgr  39294  isupgr  39319  isumgr  39328  isuspgr  39383  isusgr  39384  ushgredgedga  39452  ushgredgedgaloop  39454  issubgr  39489  subgruhgredgd  39502  subumgredg2  39503  vtxdgfval  39674  vtxdumgrval  39686  1wlk2v2elem1  39966  1wlk2v2elem2  39967  isuhgrALTV  40047  isushgrALTV  40048  elbigofrcl  40730
  Copyright terms: Public domain W3C validator