Definition df-rmo 2463

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

This definition is referenced by:  nfrmo1  2650  rmobida  2664  rmobiia  2667  rmoeq1f  2672  mormo  2689  reu5  2690  rmo5  2693  rmov  2758  rmo4  2931  rmo3f  2935  rmoan  2938  rmoim  2939  rmoimi2  2941  2reuswapdc  2942  2rmorex  2944  rmo2ilem  3053  rmo3  3055  rmob  3056  ssrmof  3219  dfdisj2  3983  dffun9  5246  fncnv  5283