Definition df-rmo

Description: Define restricted "at most one".

Note: This notation is most often used to express that ph holds for at most one element of a given class A . For this reading F/_ x A is required, though, for example, asserted when x and A are disjoint.

Should instead A depend on x , you rather assert at most one x fulfilling ph happens to be contained in the corresponding A ( x ) . This interpretation is rarely needed (see also df-ral ). (Contributed by NM, 16-Jun-2017)

	Ref	Expression
Assertion	df-rmo	⊢ ( ∃* 𝑥 ∈ 𝐴 𝜑 ↔ ∃* 𝑥 ( 𝑥 ∈ 𝐴 ∧ 𝜑 ) )

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		vx	⊢ 𝑥
1		cA	⊢ 𝐴
2		wph	⊢ 𝜑
3	2 0 1	wrmo	⊢ ∃* 𝑥 ∈ 𝐴 𝜑
4	0	cv	⊢ 𝑥
5	4 1	wcel	⊢ 𝑥 ∈ 𝐴
6	5 2	wa	⊢ ( 𝑥 ∈ 𝐴 ∧ 𝜑 )
7	6 0	wmo	⊢ ∃* 𝑥 ( 𝑥 ∈ 𝐴 ∧ 𝜑 )
8	3 7	wb	⊢ ( ∃* 𝑥 ∈ 𝐴 𝜑 ↔ ∃* 𝑥 ( 𝑥 ∈ 𝐴 ∧ 𝜑 ) )