Theorem eubidv 2489

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:   𝜑,𝑥

Allowed substitution hints:   𝜓(𝑥)   𝜒(𝑥)

Proof of Theorem eubidv

Step	Hyp	Ref	Expression
1		nfv 1840	. 2 ⊢ Ⅎ𝑥𝜑
2		eubidv.1	. 2 ⊢ (𝜑 → (𝜓 ↔ 𝜒))
3	1, 2	eubid 2487	1 ⊢ (𝜑 → (∃!𝑥𝜓 ↔ ∃!𝑥𝜒))

Syntax hints:   → wi 4   ↔ wb 196  ∃!weu 2469

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1719  ax-4 1734  ax-5 1836  ax-6 1885  ax-7 1932  ax-12 2044

This theorem depends on definitions:  df-bi 197  df-ex 1702  df-nf 1707  df-eu 2473

This theorem is referenced by:  eubii  2491  eueq2  3362  eueq3  3363  moeq3  3365  reusv2lem2  4829  reusv2lem2OLD  4830  reusv2lem5  4833  reuhypd  4855  feu  6037  dff3  6328  dff4  6329  omxpenlem  8005  dfac5lem5  8894  dfac5  8895  kmlem2  8917  kmlem12  8927  kmlem13  8928  initoval  16568  termoval  16569  isinito  16571  istermo  16572  initoid  16576  termoid  16577  initoeu1  16582  initoeu2  16587  termoeu1  16589  upxp  21336  edgnbusgreu  26156  frgrncvvdeqlem3  27029  frgreu  27049  bnj852  30699  bnj1489  30832  funpartfv  31694  fourierdlem36  39667  eu2ndop1stv  40506  dfdfat2  40515  tz6.12-afv  40557  setrec2lem1  41733