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

Theorem dmeqi 5314
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 5313 . 2 (𝐴 = 𝐵 → dom 𝐴 = dom 𝐵)
31, 2ax-mp 5 1 dom 𝐴 = dom 𝐵
Colors of variables: wff setvar class
Syntax hints:   = wceq 1481  dom cdm 5104
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1720  ax-4 1735  ax-5 1837  ax-6 1886  ax-7 1933  ax-9 1997  ax-10 2017  ax-11 2032  ax-12 2045  ax-13 2244  ax-ext 2600
This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3an 1038  df-tru 1484  df-ex 1703  df-nf 1708  df-sb 1879  df-clab 2607  df-cleq 2613  df-clel 2616  df-nfc 2751  df-rab 2918  df-v 3197  df-dif 3570  df-un 3572  df-in 3574  df-ss 3581  df-nul 3908  df-if 4078  df-sn 4169  df-pr 4171  df-op 4175  df-br 4645  df-dm 5114
This theorem is referenced by:  dmxp  5333  dmxpin  5335  rncoss  5375  rncoeq  5378  rnun  5529  rnin  5530  rnxp  5552  rnxpss  5554  imainrect  5563  dmpropg  5596  dmtpop  5599  rnsnopg  5602  fntpg  5936  opabiotadm  6247  dffv2  6258  fvopab4ndm  6293  fnreseql  6313  dmoprab  6726  reldmmpt2  6756  mpt2ndm0  6860  elmpt2cl  6861  opabn1stprc  7213  bropopvvv  7240  bropfvvvv  7242  wfrdmss  7406  wfrdmcl  7408  wfrlem16  7415  tfrlem8  7465  tfr1a  7475  tfr2a  7476  tfr2b  7477  rdgseg  7503  xpassen  8039  sbthlem5  8059  hartogslem1  8432  r1funlim  8614  r1sucg  8617  r1limg  8619  rankf  8642  hsmexlem4  9236  axdc2lem  9255  dmaddpi  9697  dmmulpi  9698  dmaddsr  9891  dmmulsr  9892  axaddf  9951  axmulf  9952  strlemor1OLD  15950  divsfval  16188  xpsfrnel2  16206  mvdco  17846  symgsssg  17868  symgfisg  17869  pmtrdifellem2  17878  psgnunilem5  17895  ismbl  23275  volres  23277  efcvx  24184  dvrelog  24364  dvlog  24378  structiedg0val  25892  snstriedgval  25911  isuhgr  25936  isushgr  25937  isupgr  25960  isumgr  25971  isuspgr  26028  isusgr  26029  ushgredgedg  26102  ushgredgedgloop  26104  lfuhgr1v0e  26127  issubgr  26144  subgruhgredgd  26157  subumgredg2  26158  vtxdgfval  26344  vtxdlfgrval  26362  vtxdginducedm1lem2  26417  vtxdginducedm1fi  26421  finsumvtxdg2ssteplem4  26425  finsumvtxdg2size  26427  wlk2v2elem1  26995  wlk2v2elem2  26996  dfhnorm2  27949  hlimcaui  28063  hhshsslem1  28094  dmadjss  28716  adjeu  28718  adj1o  28723  gsummpt2co  29754  prsdm  29934  mbfmcst  30295  eulerpartlemt  30407  0rrv  30487  coinflipspace  30516  bnj96  30909  bnj1398  31076  bnj1416  31081  bnj1450  31092  bnj1498  31103  bnj1501  31109  frrlem7  31764  noetalem3  31839  noetalem4  31840  dmscut  31892  fixun  31991  linedegen  32225  matunitlindf  33378  ssbnd  33558  ismgmOLD  33620  exidreslem  33647  dmmzp  37115  cnvrcl0  37751  dvsid  38350  dvsef  38351  dvsinax  39890  fperdvper  39896  dvcosax  39904  stoweidlem27  40007  fourierdlem57  40143  fourierdlem58  40144  fourierdlem62  40148  fourierdlem80  40166  fourierdlem94  40180  fourierdlem97  40183  fourierdlem113  40199  fouriersw  40211  fouriercn  40212  subsaliuncllem  40338  0ome  40506  hoi2toco  40584  elbigofrcl  42109
  Copyright terms: Public domain W3C validator