Theorem eubidv 2490

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

Hypothesis

Ref	Expression
eubidv.1	|- ( ph -> ( ps <-> ch ) )

Assertion

Ref	Expression
eubidv	|- ( ph -> ( E! x ps <-> E! x ch ) )

Distinct variable group:   ph, x

Allowed substitution hints:   ps( x)   ch( x)

Proof of Theorem eubidv

Step	Hyp	Ref	Expression
1		nfv 1843	. 2 |- F/ x ph
2		eubidv.1	. 2 |- ( ph -> ( ps <-> ch ) )
3	1, 2	eubid 2488	1 |- ( ph -> ( E! x ps <-> E! x ch ) )

Syntax hints:   -> wi 4   <-> wb 196   E!weu 2470

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-12 2047

This theorem depends on definitions:  df-bi 197  df-ex 1705  df-nf 1710  df-eu 2474

This theorem is referenced by:  eubii  2492  reueubd  3164  eueq2  3380  eueq3  3381  moeq3  3383  reusv2lem2  4869  reusv2lem2OLD  4870  reusv2lem5  4873  reuhypd  4895  feu  6080  dff3  6372  dff4  6373  omxpenlem  8061  dfac5lem5  8950  dfac5  8951  kmlem2  8973  kmlem12  8983  kmlem13  8984  initoval  16647  termoval  16648  isinito  16650  istermo  16651  initoid  16655  termoid  16656  initoeu1  16661  initoeu2  16666  termoeu1  16668  upxp  21426  edgnbusgreu  26269  frgrncvvdeqlem2  27164  bnj852  30991  bnj1489  31124  funpartfv  32052  fourierdlem36  40360  eu2ndop1stv  41202  dfdfat2  41211  tz6.12-afv  41253  setrec2lem1  42440