Theorem eubidv 2304

Description: Formula-building rule for uniqueness quantifier (deduction rule). (Contributed by NM, 9-Jul-1994.)

Hypothesis

Ref	Expression
eubidv.1

Assertion

Ref	Expression
eubidv

Distinct variable group:   ,

Proof of Theorem eubidv

Step	Hyp	Ref	Expression
1		nfv 1707	. 2
2		eubidv.1	. 2
3	1, 2	eubid 2302	1

Syntax hints:  ->wi 4  <->wb 184  E!weu 2282

This theorem is referenced by:  eubii  2306  eueq2  3273  eueq3  3274  moeq3  3276  reusv2lem2  4654  reusv2lem5  4657  reusv7OLD  4664  reuhypd  4679  feu  5766  dff3  6044  dff4  6045  omxpenlem  7638  dfac5lem5  8529  dfac5  8530  kmlem2  8552  kmlem12  8562  kmlem13  8563  upxp  20124  frgrancvvdeqlem3  25032  frgraeu  25054  funpartfv  29595  fourierdlem36  31925  eu2ndop1stv  32207  dfdfat2  32216  tz6.12-afv  32258  initoval  32603  termoval  32604  isinito  32606  istermo  32607  initoid  32611  termoid  32612  initoeu1  32617  initoeu2  32622  termoeu1  32624  bnj852  33979  bnj1489  34112

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-12 1854

This theorem depends on definitions:  df-bi 185  df-ex 1613  df-nf 1617  df-eu 2286