Theorem rexeqbi1dv 3063

Description: Equality deduction for restricted existential quantifier. (Contributed by NM, 18-Mar-1997.)

Hypothesis

Ref	Expression
raleqd.1

Assertion

Ref	Expression
rexeqbi1dv

Distinct variable groups:   ,   ,

Proof of Theorem rexeqbi1dv

Step	Hyp	Ref	Expression
1		rexeq 3055	. 2
2		raleqd.1	. . 3
3	2	rexbidv 2968	. 2
4	1, 3	bitrd 253	1

Syntax hints:  ->wi 4  <->wb 184  =wceq 1395  E.wrex 2808

This theorem is referenced by:  fri  4846  frsn  5075  isofrlem  6236  f1oweALT  6784  frxp  6910  1sdom  7742  oieq2  7959  zfregcl  8041  ishaus  19823  isreg  19833  isnrm  19836  lebnumlem3  21463  1vwmgra  25003  3vfriswmgra  25005  isgrpo  25198  isexid2  25327  ismndo2  25347  rngomndo  25423  pjhth  26311  frmin  29322  stoweidlem28  31810  bnj1154  34055

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-ext 2435

This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1398  df-ex 1613  df-nf 1617  df-cleq 2449  df-clel 2452  df-nfc 2607  df-rex 2813