Theorem dmeqi 5209

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 5208	. 2
3	1, 2	ax-mp 5	1

Syntax hints:  =wceq 1395  domcdm 5004

This theorem is referenced by:  dmxp  5226  dmxpin  5228  rncoss  5268  rncoeq  5271  rnun  5419  rnin  5420  rnxp  5442  rnxpss  5444  imainrect  5453  dmpropg  5486  dmtpop  5489  rnsnopg  5492  fntpg  5648  opabiotadm  5935  dffv2  5946  fvopab4ndm  5978  fnreseql  5997  dmoprab  6383  reldmmpt2  6413  mpt2ndm0  6516  elmpt2cl  6517  bropopvvv  6880  tfrlem8  7072  tfr1a  7082  tfr2a  7083  tfr2b  7084  rdgseg  7107  xpassen  7631  sbthlem5  7651  hartogslem1  7988  r1funlim  8205  r1sucg  8208  r1limg  8210  rankf  8233  hsmexlem4  8830  axdc2lem  8849  dmaddpi  9289  dmmulpi  9290  dmaddsr  9483  dmmulsr  9484  axaddf  9543  axmulf  9544  strlemor1  14724  divsfval  14944  xpsfrnel2  14962  mvdco  16470  symgsssg  16492  symgfisg  16493  pmtrdifellem2  16502  psgnunilem5  16519  ismbl  21937  volres  21939  efcvx  22844  dvrelog  23018  dvlog  23032  usgrares1  24410  usgrafilem1  24411  cusgrasizeindslem2  24474  wlkntrllem1  24561  clwwlknprop  24772  2wlkonot3v  24875  2spthonot3v  24876  eupares  24975  resgrprn  25282  ismgmOLD  25322  dfhnorm2  26039  hlimcaui  26154  hhshsslem1  26183  dmadjss  26806  adjeu  26808  adj1o  26813  prsdm  27896  mbfmcst  28230  eulerpartlemt  28310  0rrv  28390  coinflipspace  28419  ghomfo  29031  wfrlem7  29349  wfrlem9  29351  wfrlem16  29358  frrlem7  29397  nofulllem5  29466  fixun  29559  linedegen  29793  ssbnd  30284  exidreslem  30339  dmmzp  30665  dvsid  31236  dvsef  31237  dvsinax  31708  fperdvper  31715  dvcosax  31723  stoweidlem27  31809  fourierdlem57  31946  fourierdlem58  31947  fourierdlem62  31951  fourierdlem80  31969  fourierdlem94  31983  fourierdlem97  31986  fourierdlem113  32002  fouriersw  32014  fouriercn  32015  isuhgr  32366  isushgr  32367  bnj96  33923  bnj1398  34090  bnj1416  34095  bnj1450  34106  bnj1498  34117  bnj1501  34123

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1618  ax-4 1631  ax-5 1704  ax-6 1747  ax-7 1790  ax-10 1837  ax-11 1842  ax-12 1854  ax-13 1999  ax-ext 2435

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 975  df-tru 1398  df-ex 1613  df-nf 1617  df-sb 1740  df-clab 2443  df-cleq 2449  df-clel 2452  df-nfc 2607  df-rab 2816  df-v 3111  df-dif 3478  df-un 3480  df-in 3482  df-ss 3489  df-nul 3785  df-if 3942  df-sn 4030  df-pr 4032  df-op 4036  df-br 4453  df-dm 5014