Theorem rmo2i

Description: Condition implying restricted "at most one." (Contributed by NM, 17-Jun-2017)

	Ref	Expression
Hypothesis	rmo2.1	⊢ Ⅎ 𝑦 𝜑
Assertion	rmo2i	⊢ ( ∃ 𝑦 ∈ 𝐴 ∀ 𝑥 ∈ 𝐴 ( 𝜑 → 𝑥 = 𝑦 ) → ∃* 𝑥 ∈ 𝐴 𝜑 )

Proof

Step	Hyp	Ref	Expression
1		rmo2.1	⊢ Ⅎ 𝑦 𝜑
2		rexex	⊢ ( ∃ 𝑦 ∈ 𝐴 ∀ 𝑥 ∈ 𝐴 ( 𝜑 → 𝑥 = 𝑦 ) → ∃ 𝑦 ∀ 𝑥 ∈ 𝐴 ( 𝜑 → 𝑥 = 𝑦 ) )
3	1	rmo2	⊢ ( ∃* 𝑥 ∈ 𝐴 𝜑 ↔ ∃ 𝑦 ∀ 𝑥 ∈ 𝐴 ( 𝜑 → 𝑥 = 𝑦 ) )
4	2 3	sylibr	⊢ ( ∃ 𝑦 ∈ 𝐴 ∀ 𝑥 ∈ 𝐴 ( 𝜑 → 𝑥 = 𝑦 ) → ∃* 𝑥 ∈ 𝐴 𝜑 )