Theorem eubidv 2627

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

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1871  ax-4 1886  ax-5 1988  ax-6 2054  ax-7 2090  ax-12 2196

This theorem depends on definitions:  df-bi 197  df-ex 1854  df-nf 1859  df-eu 2611

This theorem is referenced by:  eubii  2629  reueubd  3303  eueq2  3521  eueq3  3522  moeq3  3524  reusv2lem2  5018  reusv2lem2OLD  5019  reusv2lem5  5022  reuhypd  5044  feu  6241  dff3  6536  dff4  6537  omxpenlem  8228  dfac5lem5  9160  dfac5  9161  kmlem2  9185  kmlem12  9195  kmlem13  9196  initoval  16868  termoval  16869  isinito  16871  istermo  16872  initoid  16876  termoid  16877  initoeu1  16882  initoeu2  16887  termoeu1  16889  upxp  21648  edgnbusgreu  26488  nbusgredgeu0  26489  frgrncvvdeqlem2  27475  bnj852  31319  bnj1489  31452  funpartfv  32379  fourierdlem36  40881  eu2ndop1stv  41726  dfdfat2  41735  tz6.12-afv  41777  setrec2lem1  42968