Definition df-rmo 2623

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

Assertion

Ref	Expression
df-rmo	⊢ (∃*x ∈ A φ ↔ ∃*x(x ∈ A ∧ φ))

Detailed syntax breakdown of Definition df-rmo

Step	Hyp	Ref	Expression
1		wph	. . 3 wff φ
2		vx	. . 3 setvar x
3		cA	. . 3 class A
4	1, 2, 3	wrmo 2618	. 2 wff ∃*x ∈ A φ
5	2	cv 1641	. . . . 5 class x
6	5, 3	wcel 1710	. . . 4 wff x ∈ A
7	6, 1	wa 358	. . 3 wff (x ∈ A ∧ φ)
8	7, 2	wmo 2205	. 2 wff ∃*x(x ∈ A ∧ φ)
9	4, 8	wb 176	1 wff (∃*x ∈ A φ ↔ ∃*x(x ∈ A ∧ φ))

This definition is referenced by:  nfrmo1  2783  nfrmod  2785  nfrmo  2787  rmobida  2799  rmobiia  2802  rmoeq1f  2807  mormo  2824  reu5  2825  rmo5  2828  rmov  2876  rmo4  3030  rmoan  3035  rmoim  3036  rmoimi2  3038  2reuswap  3039  2reu5lem2  3043  rmo2  3132  rmo3  3134  rmob  3135  fncnv  5159