Theorem rmo2

Description: Alternate definition of restricted "at most one". Note that E* x e. A ph is not equivalent to E. y e. A A. x e. A ( ph -> x = y ) (in analogy to reu6 ); to see this, let A be the empty set. However, one direction of this pattern holds; see rmo2i . (Contributed by NM, 17-Jun-2017)

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

Proof

Step	Hyp	Ref	Expression
1		rmo2.1	⊢ Ⅎ 𝑦 𝜑
2		df-rmo	⊢ ( ∃* 𝑥 ∈ 𝐴 𝜑 ↔ ∃* 𝑥 ( 𝑥 ∈ 𝐴 ∧ 𝜑 ) )
3		nfv	⊢ Ⅎ 𝑦 𝑥 ∈ 𝐴
4	3 1	nfan	⊢ Ⅎ 𝑦 ( 𝑥 ∈ 𝐴 ∧ 𝜑 )
5	4	mof	⊢ ( ∃* 𝑥 ( 𝑥 ∈ 𝐴 ∧ 𝜑 ) ↔ ∃ 𝑦 ∀ 𝑥 ( ( 𝑥 ∈ 𝐴 ∧ 𝜑 ) → 𝑥 = 𝑦 ) )
6		impexp	⊢ ( ( ( 𝑥 ∈ 𝐴 ∧ 𝜑 ) → 𝑥 = 𝑦 ) ↔ ( 𝑥 ∈ 𝐴 → ( 𝜑 → 𝑥 = 𝑦 ) ) )
7	6	albii	⊢ ( ∀ 𝑥 ( ( 𝑥 ∈ 𝐴 ∧ 𝜑 ) → 𝑥 = 𝑦 ) ↔ ∀ 𝑥 ( 𝑥 ∈ 𝐴 → ( 𝜑 → 𝑥 = 𝑦 ) ) )
8		df-ral	⊢ ( ∀ 𝑥 ∈ 𝐴 ( 𝜑 → 𝑥 = 𝑦 ) ↔ ∀ 𝑥 ( 𝑥 ∈ 𝐴 → ( 𝜑 → 𝑥 = 𝑦 ) ) )
9	7 8	bitr4i	⊢ ( ∀ 𝑥 ( ( 𝑥 ∈ 𝐴 ∧ 𝜑 ) → 𝑥 = 𝑦 ) ↔ ∀ 𝑥 ∈ 𝐴 ( 𝜑 → 𝑥 = 𝑦 ) )
10	9	exbii	⊢ ( ∃ 𝑦 ∀ 𝑥 ( ( 𝑥 ∈ 𝐴 ∧ 𝜑 ) → 𝑥 = 𝑦 ) ↔ ∃ 𝑦 ∀ 𝑥 ∈ 𝐴 ( 𝜑 → 𝑥 = 𝑦 ) )
11	2 5 10	3bitri	⊢ ( ∃* 𝑥 ∈ 𝐴 𝜑 ↔ ∃ 𝑦 ∀ 𝑥 ∈ 𝐴 ( 𝜑 → 𝑥 = 𝑦 ) )