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

Theorem dmeqi 5357
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 5356 . 2 (𝐴 = 𝐵 → dom 𝐴 = dom 𝐵)
31, 2ax-mp 5 1 dom 𝐴 = dom 𝐵
Colors of variables: wff setvar class
Syntax hints:   = wceq 1523  dom cdm 5143
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777  ax-5 1879  ax-6 1945  ax-7 1981  ax-9 2039  ax-10 2059  ax-11 2074  ax-12 2087  ax-13 2282  ax-ext 2631
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3an 1056  df-tru 1526  df-ex 1745  df-nf 1750  df-sb 1938  df-clab 2638  df-cleq 2644  df-clel 2647  df-nfc 2782  df-rab 2950  df-v 3233  df-dif 3610  df-un 3612  df-in 3614  df-ss 3621  df-nul 3949  df-if 4120  df-sn 4211  df-pr 4213  df-op 4217  df-br 4686  df-dm 5153
This theorem is referenced by:  dmxp  5376  dmxpin  5378  rncoss  5418  rncoeq  5421  rnun  5576  rnin  5577  rnxp  5599  rnxpss  5601  imainrect  5610  dmpropg  5644  dmtpop  5647  rnsnopg  5650  fntpg  5986  opabiotadm  6299  dffv2  6310  fvopab4ndm  6346  fnreseql  6367  dmoprab  6783  reldmmpt2  6813  mpt2ndm0  6917  elmpt2cl  6918  opabn1stprc  7272  bropopvvv  7300  bropfvvvv  7302  wfrdmss  7466  wfrdmcl  7468  wfrlem16  7475  tfrlem8  7525  tfr1a  7535  tfr2a  7536  tfr2b  7537  rdgseg  7563  xpassen  8095  sbthlem5  8115  hartogslem1  8488  r1funlim  8667  r1sucg  8670  r1limg  8672  rankf  8695  hsmexlem4  9289  axdc2lem  9308  dmaddpi  9750  dmmulpi  9751  dmaddsr  9944  dmmulsr  9945  axaddf  10004  axmulf  10005  strlemor1OLD  16016  divsfval  16254  xpsfrnel2  16272  mvdco  17911  symgsssg  17933  symgfisg  17934  pmtrdifellem2  17943  psgnunilem5  17960  ismbl  23340  volres  23342  efcvx  24248  dvrelog  24428  dvlog  24442  structiedg0val  25956  snstriedgval  25975  isuhgr  26000  isushgr  26001  isupgr  26024  isumgr  26035  isuspgr  26092  isusgr  26093  ushgredgedg  26166  ushgredgedgloop  26168  lfuhgr1v0e  26191  issubgr  26208  subgruhgredgd  26221  subumgredg2  26222  vtxdgfval  26419  vtxdlfgrval  26437  vtxdginducedm1lem2  26492  vtxdginducedm1fi  26496  finsumvtxdg2ssteplem4  26500  finsumvtxdg2size  26502  wlk2v2elem1  27133  wlk2v2elem2  27134  dfhnorm2  28107  hlimcaui  28221  hhshsslem1  28252  dmadjss  28874  adjeu  28876  adj1o  28881  gsummpt2co  29908  prsdm  30088  mbfmcst  30449  eulerpartlemt  30561  0rrv  30641  coinflipspace  30670  bnj96  31061  bnj1398  31228  bnj1416  31233  bnj1450  31244  bnj1498  31255  bnj1501  31261  frrlem7  31915  noetalem3  31990  noetalem4  31991  dmscut  32043  fixun  32141  linedegen  32375  matunitlindf  33537  ssbnd  33717  ismgmOLD  33779  exidreslem  33806  n0el2  34244  dmcoss3  34343  dmcoels  34347  dmmzp  37613  cnvrcl0  38249  dvsid  38847  dvsef  38848  dvsinax  40445  fperdvper  40451  dvcosax  40459  stoweidlem27  40562  fourierdlem57  40698  fourierdlem58  40699  fourierdlem62  40703  fourierdlem80  40721  fourierdlem94  40735  fourierdlem97  40738  fourierdlem113  40754  fouriersw  40766  fouriercn  40767  subsaliuncllem  40893  0ome  41064  hoi2toco  41142  elbigofrcl  42669
  Copyright terms: Public domain W3C validator