Theorem dmeqi 5012

Description: Equality inference for domain. (Contributed by NM, 4-Mar-2004.)

Hypothesis

Ref	Expression
dmeqi.1

Assertion

Ref	Expression
dmeqi

Proof of Theorem dmeqi

Step	Hyp	Ref	Expression
1		dmeqi.1	. 2
2		dmeq 5011	. 2
3	1, 2	ax-mp 5	1

Syntax hints:  =wceq 1687  domcdm 4811

This theorem is referenced by:  dmxp  5029  dmxpin  5031  rncoss  5071  rncoeq  5074  rnun  5217  rnin  5218  rnxp  5240  rnxpss  5242  imainrect  5251  dmpropg  5284  dmtpop  5287  rnsnopg  5290  fntpg  5443  opabiotadm  5723  dffv2  5734  fvopab4ndm  5764  fnreseql  5783  dmoprab  6141  reldmmpt2  6171  elmpt2cl  6274  bropopvvv  6622  mpt2ndm0  6701  tfrlem8  6802  tfr1a  6812  tfr2a  6813  tfr2b  6814  rdgseg  6837  xpassen  7364  sbthlem5  7384  hartogslem1  7703  r1funlim  7920  r1sucg  7923  r1limg  7925  rankf  7948  hsmexlem4  8545  axdc2lem  8564  dmaddpi  9005  dmmulpi  9006  dmaddsr  9198  dmmulsr  9199  axaddf  9258  axmulf  9259  strlemor1  14205  divsfval  14425  xpsfrnel2  14443  mvdco  15888  symgsssg  15910  symgfisg  15911  pmtrdifellem2  15920  psgnunilem5  15937  ismbl  20709  volres  20711  efcvx  21655  dvrelog  21823  dvlog  21837  usgrares1  23002  usgrafilem1  23003  cusgrasizeindslem2  23061  wlkntrllem1  23137  eupares  23275  resgrprn  23446  ismgm  23486  dfhnorm2  24203  hlimcaui  24318  hhshsslem1  24347  dmadjss  24970  adjeu  24972  adj1o  24977  gsummpt2co  25956  prsdm  26053  mbfmcst  26383  eulerpartlemt  26457  0rrv  26537  coinflipspace  26566  ghomfo  27012  wfrlem7  27432  wfrlem9  27434  wfrlem16  27441  frrlem7  27480  nofulllem5  27549  fixun  27642  linedegen  27876  ssbnd  28358  exidreslem  28413  dmmzp  28742  dvsid  29278  dvsef  29279  stoweidlem27  29496  2wlkonot3v  30068  2spthonot3v  30069  clwwlknprop  30109  bnj96  31436  bnj1398  31603  bnj1416  31608  bnj1450  31619  bnj1498  31630  bnj1501  31636

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1586  ax-4 1597  ax-5 1661  ax-6 1701  ax-7 1721  ax-10 1768  ax-11 1773  ax-12 1785  ax-13 1934  ax-ext 2403

This theorem depends on definitions:  df-bi 179  df-or 363  df-an 364  df-3an 952  df-tru 1355  df-ex 1582  df-nf 1585  df-sb 1694  df-clab 2409  df-cleq 2415  df-clel 2418  df-nfc 2547  df-rab 2703  df-v 2953  df-dif 3308  df-un 3310  df-in 3312  df-ss 3319  df-nul 3615  df-if 3769  df-sn 3859  df-pr 3860  df-op 3862  df-br 4268  df-dm 4821