Theorem eubidv 1384

Description: Formula-building rule for uniqueness quantifier (deduction rule).

Hypothesis

Ref	Expression
eubidv.1	⊢ (φ → (ψ ↔ χ))

Assertion

Ref	Expression
eubidv	⊢ (φ → (∃!xψ ↔ ∃!xχ))

Distinct variable group:   φ,x

Proof of Theorem eubidv

Step	Hyp	Ref	Expression
1		ax-17 969	. 2 ⊢ (φ → ∀xφ)
2		eubidv.1	. 2 ⊢ (φ → (ψ ↔ χ))
3	1, 2	eubid 1383	1 ⊢ (φ → (∃!xψ ↔ ∃!xχ))

Syntax hints:   → wi 3   ↔ wb 146  ∃!weu 1378

This theorem is referenced by:  reubidva 1776  eueq2 1914  eueq3 1915  moeq3 1917  reuhyp 2900  fneu 3584  feu 3638  tz6.12-2 3730  fnbrfvb 3744  dff2 3808  dff3 3809  aceq5lem5 4719  aceq5 4720  kmlem2 4746  kmlem12 4756  kmlem13 4757  supxrre 6038  pjtheut 9174

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-gen 961  ax-17 969  ax-4 971  ax-5o 973

This theorem depends on definitions:  df-bi 147  df-an 225  df-ex 979  df-eu 1380

Copyright terms: Public domain