Definition df-rmo 2451

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

This definition is referenced by:  nfrmo1  2637  rmobida  2651  rmobiia  2654  rmoeq1f  2659  mormo  2676  reu5  2677  rmo5  2680  rmov  2745  rmo4  2918  rmo3f  2922  rmoan  2925  rmoim  2926  rmoimi2  2928  2reuswapdc  2929  2rmorex  2931  rmo2ilem  3039  rmo3  3041  rmob  3042  ssrmof  3204  dfdisj2  3960  dffun9  5216  fncnv  5253