Definition df-rmo 2368

Description: Define restricted "at most one". (Contributed by NM, 16-Jun-2017.)

Assertion

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

Detailed syntax breakdown of Definition df-rmo

Step	Hyp	Ref	Expression
1		wph	. . 3 wff 𝜑
2		vx	. . 3 setvar 𝑥
3		cA	. . 3 class 𝐴
4	1, 2, 3	wrmo 2363	. 2 wff ∃*𝑥 ∈ 𝐴 𝜑
5	2	cv 1289	. . . . 5 class 𝑥
6	5, 3	wcel 1439	. . . 4 wff 𝑥 ∈ 𝐴
7	6, 1	wa 103	. . 3 wff (𝑥 ∈ 𝐴 ∧ 𝜑)
8	7, 2	wmo 1950	. 2 wff ∃*𝑥(𝑥 ∈ 𝐴 ∧ 𝜑)
9	4, 8	wb 104	1 wff (∃*𝑥 ∈ 𝐴 𝜑 ↔ ∃*𝑥(𝑥 ∈ 𝐴 ∧ 𝜑))

This definition is referenced by:  nfrmo1  2540  rmobida  2554  rmobiia  2557  rmoeq1f  2562  mormo  2579  reu5  2580  rmo5  2583  rmov  2640  rmo4  2809  rmo3f  2813  rmoan  2816  rmoim  2817  rmoimi2  2819  2reuswapdc  2820  2rmorex  2822  rmo2ilem  2929  rmo3  2931  rmob  2932  dfdisj2  3830  dffun9  5057  fncnv  5093