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

Theorem dmeqi 5234
Description: Equality inference for domain. (Contributed by NM, 4-Mar-2004.)
Hypothesis
Ref Expression
dmeqi.1 𝐴 = 𝐵
Assertion
Ref Expression
dmeqi dom 𝐴 = dom 𝐵

Proof of Theorem dmeqi
StepHypRef Expression
1 dmeqi.1 . 2 𝐴 = 𝐵
2 dmeq 5233 . 2 (𝐴 = 𝐵 → dom 𝐴 = dom 𝐵)
31, 2ax-mp 5 1 dom 𝐴 = dom 𝐵
Colors of variables: wff setvar class
Syntax hints:   = wceq 1474  dom cdm 5028
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1712  ax-4 1727  ax-5 1826  ax-6 1874  ax-7 1921  ax-10 2005  ax-11 2020  ax-12 2033  ax-13 2233  ax-ext 2589
This theorem depends on definitions:  df-bi 195  df-or 383  df-an 384  df-3an 1032  df-tru 1477  df-ex 1695  df-nf 1700  df-sb 1867  df-clab 2596  df-cleq 2602  df-clel 2605  df-nfc 2739  df-rab 2904  df-v 3174  df-dif 3542  df-un 3544  df-in 3546  df-ss 3553  df-nul 3874  df-if 4036  df-sn 4125  df-pr 4127  df-op 4131  df-br 4578  df-dm 5038
This theorem is referenced by:  dmxp  5252  dmxpin  5254  rncoss  5294  rncoeq  5297  rnun  5446  rnin  5447  rnxp  5469  rnxpss  5471  imainrect  5480  dmpropg  5512  dmtpop  5515  rnsnopg  5518  fntpg  5848  opabiotadm  6155  dffv2  6166  fvopab4ndm  6200  fnreseql  6220  dmoprab  6617  reldmmpt2  6647  mpt2ndm0  6750  elmpt2cl  6751  bropopvvv  7119  bropfvvvv  7121  wfrdmss  7285  wfrdmcl  7287  wfrlem16  7294  tfrlem8  7344  tfr1a  7354  tfr2a  7355  tfr2b  7356  rdgseg  7382  xpassen  7916  sbthlem5  7936  hartogslem1  8307  r1funlim  8489  r1sucg  8492  r1limg  8494  rankf  8517  hsmexlem4  9111  axdc2lem  9130  dmaddpi  9568  dmmulpi  9569  dmaddsr  9762  dmmulsr  9763  axaddf  9822  axmulf  9823  strlemor1  15742  divsfval  15976  xpsfrnel2  15994  mvdco  17634  symgsssg  17656  symgfisg  17657  pmtrdifellem2  17666  psgnunilem5  17683  ismbl  23018  volres  23020  efcvx  23924  dvrelog  24100  dvlog  24114  usgrares1  25705  usgrafilem1  25706  cusgrasizeindslem1  25768  wlkntrllem1  25855  clwwlknprop  26066  2wlkonot3v  26168  2spthonot3v  26169  eupares  26268  dfhnorm2  27169  hlimcaui  27283  hhshsslem1  27314  dmadjss  27936  adjeu  27938  adj1o  27943  gsummpt2co  28917  prsdm  29094  mbfmcst  29454  eulerpartlemt  29566  0rrv  29646  coinflipspace  29675  bnj96  29995  bnj1398  30162  bnj1416  30167  bnj1450  30178  bnj1498  30189  bnj1501  30195  frrlem7  30840  nofulllem5  30911  fixun  30992  linedegen  31226  matunitlindf  32373  ssbnd  32553  ismgmOLD  32615  exidreslem  32642  dmmzp  36110  cnvrcl0  36747  dvsid  37348  dvsef  37349  dvsinax  38598  fperdvper  38605  dvcosax  38613  stoweidlem27  38717  fourierdlem57  38853  fourierdlem58  38854  fourierdlem62  38858  fourierdlem80  38876  fourierdlem94  38890  fourierdlem97  38893  fourierdlem113  38909  fouriersw  38921  fouriercn  38922  subsaliuncllem  39048  0ome  39216  hoi2toco  39294  opabn1stprc  40126  structiedg0val  40250  snstriedgval  40264  isuhgr  40277  isushgr  40278  isupgr  40305  isumgr  40315  isuspgr  40377  isusgr  40378  ushgredgedga  40451  ushgredgedgaloop  40453  lfuhgr1v0e  40475  issubgr  40490  subgruhgredgd  40503  subumgredg2  40504  vtxdgfval  40678  vtxdlfgrval  40695  1wlk2v2elem1  41317  1wlk2v2elem2  41318  elbigofrcl  42137
  Copyright terms: Public domain W3C validator