Theorem eubii

Description: Introduce unique existential quantifier to both sides of an equivalence. (Contributed by NM, 9-Jul-1994) (Revised by Mario Carneiro, 6-Oct-2016) Avoid ax-5 . (Revised by Wolf Lammen, 27-Sep-2023)

	Ref	Expression
Hypothesis	eubii.1	⊢ ( 𝜑 ↔ 𝜓 )
Assertion	eubii	⊢ ( ∃! 𝑥 𝜑 ↔ ∃! 𝑥 𝜓 )

Proof

Step	Hyp	Ref	Expression
1		eubii.1	⊢ ( 𝜑 ↔ 𝜓 )
2	1	exbii	⊢ ( ∃ 𝑥 𝜑 ↔ ∃ 𝑥 𝜓 )
3	1	mobii	⊢ ( ∃* 𝑥 𝜑 ↔ ∃* 𝑥 𝜓 )
4	2 3	anbi12i	⊢ ( ( ∃ 𝑥 𝜑 ∧ ∃* 𝑥 𝜑 ) ↔ ( ∃ 𝑥 𝜓 ∧ ∃* 𝑥 𝜓 ) )
5		df-eu	⊢ ( ∃! 𝑥 𝜑 ↔ ( ∃ 𝑥 𝜑 ∧ ∃* 𝑥 𝜑 ) )
6		df-eu	⊢ ( ∃! 𝑥 𝜓 ↔ ( ∃ 𝑥 𝜓 ∧ ∃* 𝑥 𝜓 ) )
7	4 5 6	3bitr4i	⊢ ( ∃! 𝑥 𝜑 ↔ ∃! 𝑥 𝜓 )