Theorem eubi

Description: Equivalence theorem for the unique existential quantifier. Theorem *14.271 in WhiteheadRussell p. 192. (Contributed by Andrew Salmon, 11-Jul-2011) Reduce dependencies on axioms. (Revised by BJ, 7-Oct-2022)

	Ref	Expression
Assertion	eubi	⊢ ( ∀ 𝑥 ( 𝜑 ↔ 𝜓 ) → ( ∃! 𝑥 𝜑 ↔ ∃! 𝑥 𝜓 ) )

Proof

Step	Hyp	Ref	Expression
1		exbi	⊢ ( ∀ 𝑥 ( 𝜑 ↔ 𝜓 ) → ( ∃ 𝑥 𝜑 ↔ ∃ 𝑥 𝜓 ) )
2		mobi	⊢ ( ∀ 𝑥 ( 𝜑 ↔ 𝜓 ) → ( ∃* 𝑥 𝜑 ↔ ∃* 𝑥 𝜓 ) )
3	1 2	anbi12d	⊢ ( ∀ 𝑥 ( 𝜑 ↔ 𝜓 ) → ( ( ∃ 𝑥 𝜑 ∧ ∃* 𝑥 𝜑 ) ↔ ( ∃ 𝑥 𝜓 ∧ ∃* 𝑥 𝜓 ) ) )
4		df-eu	⊢ ( ∃! 𝑥 𝜑 ↔ ( ∃ 𝑥 𝜑 ∧ ∃* 𝑥 𝜑 ) )
5		df-eu	⊢ ( ∃! 𝑥 𝜓 ↔ ( ∃ 𝑥 𝜓 ∧ ∃* 𝑥 𝜓 ) )
6	3 4 5	3bitr4g	⊢ ( ∀ 𝑥 ( 𝜑 ↔ 𝜓 ) → ( ∃! 𝑥 𝜑 ↔ ∃! 𝑥 𝜓 ) )