Theorem eu4

Description: Uniqueness using implicit substitution. (Contributed by NM, 26-Jul-1995)

	Ref	Expression
Hypothesis	eu4.1	⊢ ( 𝑥 = 𝑦 → ( 𝜑 ↔ 𝜓 ) )
Assertion	eu4	⊢ ( ∃! 𝑥 𝜑 ↔ ( ∃ 𝑥 𝜑 ∧ ∀ 𝑥 ∀ 𝑦 ( ( 𝜑 ∧ 𝜓 ) → 𝑥 = 𝑦 ) ) )

Proof

Step	Hyp	Ref	Expression
1		eu4.1	⊢ ( 𝑥 = 𝑦 → ( 𝜑 ↔ 𝜓 ) )
2		df-eu	⊢ ( ∃! 𝑥 𝜑 ↔ ( ∃ 𝑥 𝜑 ∧ ∃* 𝑥 𝜑 ) )
3	1	mo4	⊢ ( ∃* 𝑥 𝜑 ↔ ∀ 𝑥 ∀ 𝑦 ( ( 𝜑 ∧ 𝜓 ) → 𝑥 = 𝑦 ) )
4	3	anbi2i	⊢ ( ( ∃ 𝑥 𝜑 ∧ ∃* 𝑥 𝜑 ) ↔ ( ∃ 𝑥 𝜑 ∧ ∀ 𝑥 ∀ 𝑦 ( ( 𝜑 ∧ 𝜓 ) → 𝑥 = 𝑦 ) ) )
5	2 4	bitri	⊢ ( ∃! 𝑥 𝜑 ↔ ( ∃ 𝑥 𝜑 ∧ ∀ 𝑥 ∀ 𝑦 ( ( 𝜑 ∧ 𝜓 ) → 𝑥 = 𝑦 ) ) )