Definition df-rmo 2536

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 2531	. 2 wff ∃*𝑥 ∈ 𝐴 𝜑
5	2	cv 1401	. . . . 5 class 𝑥
6	5, 3	wcel 2209	. . . 4 wff 𝑥 ∈ 𝐴
7	6, 1	wa 104	. . 3 wff (𝑥 ∈ 𝐴 ∧ 𝜑)
8	7, 2	wmo 2087	. 2 wff ∃*𝑥(𝑥 ∈ 𝐴 ∧ 𝜑)
9	4, 8	wb 105	1 wff (∃*𝑥 ∈ 𝐴 𝜑 ↔ ∃*𝑥(𝑥 ∈ 𝐴 ∧ 𝜑))

This definition is referenced by:  nfrmo1  2724  cbvrmow  2735  rmobida  2740  rmobiia  2743  rmoeq1f  2748  mormo  2769  reu5  2770  rmo5  2773  rmov  2842  rmo4  3019  rmo3f  3023  rmoan  3026  rmoim  3027  rmoimi2  3029  2reuswapdc  3030  2rmorex  3032  rmo2ilem  3142  rmo3  3144  rmob  3145  ssrmof  3311  dfdisj2  4106  dffun9  5404  fncnv  5445