Theorem eubidv 2478

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 1830	. 2 ⊢ Ⅎ𝑥𝜑
2		eubidv.1	. 2 ⊢ (𝜑 → (𝜓 ↔ 𝜒))
3	1, 2	eubid 2476	1 ⊢ (𝜑 → (∃!𝑥𝜓 ↔ ∃!𝑥𝜒))

Syntax hints:   → wi 4   ↔ wb 195  ∃!weu 2458

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-12 2034

This theorem depends on definitions:  df-bi 196  df-ex 1696  df-nf 1701  df-eu 2462

This theorem is referenced by:  eubii  2480  eueq2  3347  eueq3  3348  moeq3  3350  reusv2lem2  4795  reusv2lem2OLD  4796  reusv2lem5  4799  reuhypd  4821  feu  5993  dff3  6280  dff4  6281  omxpenlem  7946  dfac5lem5  8833  dfac5  8834  kmlem2  8856  kmlem12  8866  kmlem13  8867  initoval  16470  termoval  16471  isinito  16473  istermo  16474  initoid  16478  termoid  16479  initoeu1  16484  initoeu2  16489  termoeu1  16491  upxp  21236  frgrancvvdeqlem3  26559  frgraeu  26581  bnj852  30245  bnj1489  30378  funpartfv  31222  fourierdlem36  39036  eu2ndop1stv  39851  dfdfat2  39860  tz6.12-afv  39902  edgnbusgreu  40595  frgrncvvdeqlem3  41471  frgreu  41491  setrec2lem1  42239