Theorem reu4

Description: Restricted uniqueness using implicit substitution. (Contributed by NM, 23-Nov-1994)

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

Proof

Step	Hyp	Ref	Expression
1		rmo4.1	⊢ ( 𝑥 = 𝑦 → ( 𝜑 ↔ 𝜓 ) )
2		reu5	⊢ ( ∃! 𝑥 ∈ 𝐴 𝜑 ↔ ( ∃ 𝑥 ∈ 𝐴 𝜑 ∧ ∃* 𝑥 ∈ 𝐴 𝜑 ) )
3	1	rmo4	⊢ ( ∃* 𝑥 ∈ 𝐴 𝜑 ↔ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ( ( 𝜑 ∧ 𝜓 ) → 𝑥 = 𝑦 ) )
4	3	anbi2i	⊢ ( ( ∃ 𝑥 ∈ 𝐴 𝜑 ∧ ∃* 𝑥 ∈ 𝐴 𝜑 ) ↔ ( ∃ 𝑥 ∈ 𝐴 𝜑 ∧ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ( ( 𝜑 ∧ 𝜓 ) → 𝑥 = 𝑦 ) ) )
5	2 4	bitri	⊢ ( ∃! 𝑥 ∈ 𝐴 𝜑 ↔ ( ∃ 𝑥 ∈ 𝐴 𝜑 ∧ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ( ( 𝜑 ∧ 𝜓 ) → 𝑥 = 𝑦 ) ) )