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

Theorem dmeqi 5030
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 5029 . 2  |-  ( A  =  B  ->  dom  A  =  dom  B )
31, 2ax-mp 8 1  |-  dom  A  =  dom  B
Colors of variables: wff set class
Syntax hints:    = wceq 1649   dom cdm 4837
This theorem is referenced by:  dmxp  5047  dmxpin  5049  rncoss  5095  rncoeq  5098  rnun  5239  rnin  5240  rnxp  5258  rnxpss  5260  imainrect  5271  dmpropg  5302  dmtpop  5305  rnsnopg  5308  fntpg  5465  dffv2  5755  fvopab4ndm  5784  fnreseql  5799  dmoprab  6113  reldmmpt2  6140  elmpt2cl  6247  bropopvvv  6385  mpt2ndm0  6432  opabiotadm  6496  tfrlem8  6604  tfr1a  6614  tfr2a  6615  tfr2b  6616  rdgseg  6639  xpassen  7161  sbthlem5  7180  hartogslem1  7467  r1funlim  7648  r1sucg  7651  r1limg  7653  rankf  7676  hsmexlem4  8265  axdc2lem  8284  dmaddpi  8723  dmmulpi  8724  dmaddsr  8916  dmmulsr  8917  axaddf  8976  axmulf  8977  strlemor1  13511  divsfval  13727  xpsfrnel2  13745  ismbl  19375  volres  19377  efcvx  20318  dvrelog  20481  dvlog  20495  usgrares1  21377  usgrafilem1  21378  cusgrasizeindslem2  21436  wlkntrllem1  21512  eupares  21650  resgrprn  21821  ismgm  21861  dfhnorm2  22577  hlimcaui  22692  hhshsslem1  22720  dmadjss  23343  adjeu  23345  adj1o  23350  mbfmcst  24562  0rrv  24662  coinflipspace  24691  ghomfo  25055  wfrlem7  25476  wfrlem9  25478  wfrlem16  25485  frrlem7  25505  nofulllem5  25574  fixun  25663  linedegen  25981  ssbnd  26387  exidreslem  26442  dmmzp  26680  mvdco  27256  symgsssg  27276  symgfisg  27277  psgnunilem5  27285  dvsid  27416  dvsef  27417  stoweidlem27  27643  2wlkonot3v  28072  2spthonot3v  28073  bnj96  28942  bnj1398  29109  bnj1416  29114  bnj1450  29125  bnj1498  29136  bnj1501  29142
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1662  ax-8 1683  ax-6 1740  ax-7 1745  ax-11 1757  ax-12 1946  ax-ext 2385
This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-3an 938  df-tru 1325  df-ex 1548  df-nf 1551  df-sb 1656  df-clab 2391  df-cleq 2397  df-clel 2400  df-nfc 2529  df-rab 2675  df-v 2918  df-dif 3283  df-un 3285  df-in 3287  df-ss 3294  df-nul 3589  df-if 3700  df-sn 3780  df-pr 3781  df-op 3783  df-br 4173  df-dm 4847
  Copyright terms: Public domain W3C validator