Definition df-rmo 2425

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

This definition is referenced by:  nfrmo1  2606  rmobida  2620  rmobiia  2623  rmoeq1f  2628  mormo  2645  reu5  2646  rmo5  2649  rmov  2709  rmo4  2881  rmo3f  2885  rmoan  2888  rmoim  2889  rmoimi2  2891  2reuswapdc  2892  2rmorex  2894  rmo2ilem  3002  rmo3  3004  rmob  3005  ssrmof  3165  dfdisj2  3916  dffun9  5160  fncnv  5197