Definition df-rmo 2424

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 2419	. 2 wff ∃*𝑥 ∈ 𝐴 𝜑
5	2	cv 1330	. . . . 5 class 𝑥
6	5, 3	wcel 1480	. . . 4 wff 𝑥 ∈ 𝐴
7	6, 1	wa 103	. . 3 wff (𝑥 ∈ 𝐴 ∧ 𝜑)
8	7, 2	wmo 2000	. 2 wff ∃*𝑥(𝑥 ∈ 𝐴 ∧ 𝜑)
9	4, 8	wb 104	1 wff (∃*𝑥 ∈ 𝐴 𝜑 ↔ ∃*𝑥(𝑥 ∈ 𝐴 ∧ 𝜑))

This definition is referenced by:  nfrmo1  2603  rmobida  2617  rmobiia  2620  rmoeq1f  2625  mormo  2642  reu5  2643  rmo5  2646  rmov  2706  rmo4  2877  rmo3f  2881  rmoan  2884  rmoim  2885  rmoimi2  2887  2reuswapdc  2888  2rmorex  2890  rmo2ilem  2998  rmo3  3000  rmob  3001  ssrmof  3160  dfdisj2  3908  dffun9  5152  fncnv  5189