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

Theorem dmeqi 5772
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 5771 . 2 (𝐴 = 𝐵 → dom 𝐴 = dom 𝐵)
31, 2ax-mp 5 1 dom 𝐴 = dom 𝐵
Colors of variables: wff setvar class
Syntax hints:   = wceq 1530  dom cdm 5554
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1904  ax-6 1963  ax-7 2008  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2153  ax-12 2169  ax-ext 2798
This theorem depends on definitions:  df-bi 208  df-an 397  df-or 844  df-3an 1083  df-tru 1533  df-ex 1774  df-nf 1778  df-sb 2063  df-clab 2805  df-cleq 2819  df-clel 2898  df-nfc 2968  df-rab 3152  df-v 3502  df-dif 3943  df-un 3945  df-in 3947  df-ss 3956  df-nul 4296  df-if 4471  df-sn 4565  df-pr 4567  df-op 4571  df-br 5064  df-dm 5564
This theorem is referenced by:  dmxp  5798  dmxpin  5800  rncoss  5842  rncoeq  5845  rnun  6003  rnin  6004  rnxp  6026  rnxpss  6028  imainrect  6037  dmpropg  6071  dmtpop  6074  rnsnopg  6077  fntpg  6413  opabiotadm  6744  dffv2  6755  fvopab4ndm  6795  fnreseql  6816  dmoprab  7249  reldmmpo  7279  mpondm0  7380  elmpocl  7381  opabn1stprc  7752  bropopvvv  7781  bropfvvvv  7783  wfrdmss  7957  wfrdmcl  7959  wfrlem16  7966  tfrlem8  8016  tfr1a  8026  tfr2a  8027  tfr2b  8028  rdgseg  8054  xpassen  8605  sbthlem5  8625  hartogslem1  9000  r1funlim  9189  r1sucg  9192  r1limg  9194  rankf  9217  hsmexlem4  9845  axdc2lem  9864  dmaddpi  10306  dmmulpi  10307  dmaddsr  10501  dmmulsr  10502  axaddf  10561  axmulf  10562  divsfval  16815  mvdco  18509  symgsssg  18531  symgfisg  18532  pmtrdifellem2  18541  psgnunilem5  18558  ismbl  24061  volres  24063  efcvx  24971  dvrelog  25152  dvlog  25166  structiedg0val  26740  snstriedgval  26756  isuhgr  26778  isushgr  26779  isupgr  26802  isumgr  26813  isuspgr  26870  isusgr  26871  ushgredgedg  26944  ushgredgedgloop  26946  lfuhgr1v0e  26969  issubgr  26986  subgruhgredgd  26999  subumgredg2  27000  vtxdgfval  27182  vtxdlfgrval  27200  vtxdginducedm1lem2  27255  vtxdginducedm1fi  27259  finsumvtxdg2ssteplem4  27263  finsumvtxdg2size  27265  wlk2v2elem1  27867  dfhnorm2  28832  hlimcaui  28946  hhshsslem1  28977  dmadjss  29597  adjeu  29599  adj1o  29604  gsummpt2co  30619  cycpmrn  30718  tocyccntz  30719  prsdm  31062  mbfmcst  31422  eulerpartlemt  31534  0rrv  31614  coinflipspace  31643  bnj96  32042  bnj1398  32209  bnj1416  32214  bnj1450  32225  bnj1498  32236  bnj1501  32242  fmla  32531  fmla0  32532  gonan0  32542  satffunlem2lem2  32556  frrlem7  33032  frrlem14  33039  noetalem3  33122  noetalem4  33123  dmscut  33175  fixun  33273  linedegen  33507  matunitlindf  34776  ssbnd  34953  ismgmOLD  35015  exidreslem  35042  n0el2  35477  dmcoss3  35579  dmcoels  35583  dmmzp  39214  cnvrcl0  39869  dvsid  40547  dvsef  40548  dvsinax  42081  fperdvper  42087  dvcosax  42095  stoweidlem27  42197  fourierdlem57  42333  fourierdlem58  42334  fourierdlem62  42338  fourierdlem80  42356  fourierdlem94  42370  fourierdlem97  42373  fourierdlem113  42389  fouriersw  42401  fouriercn  42402  subsaliuncllem  42525  0ome  42696  hoi2toco  42774  elbigofrcl  44512
  Copyright terms: Public domain W3C validator