Definition df-rmo 2493

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

This definition is referenced by:  nfrmo1  2680  rmobida  2694  rmobiia  2697  rmoeq1f  2702  mormo  2723  reu5  2724  rmo5  2727  rmov  2794  rmo4  2970  rmo3f  2974  rmoan  2977  rmoim  2978  rmoimi2  2980  2reuswapdc  2981  2rmorex  2983  rmo2ilem  3092  rmo3  3094  rmob  3095  ssrmof  3260  dfdisj2  4029  dffun9  5309  fncnv  5349