Definition df-rmo 2456

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

This definition is referenced by:  nfrmo1  2642  rmobida  2656  rmobiia  2659  rmoeq1f  2664  mormo  2681  reu5  2682  rmo5  2685  rmov  2750  rmo4  2923  rmo3f  2927  rmoan  2930  rmoim  2931  rmoimi2  2933  2reuswapdc  2934  2rmorex  2936  rmo2ilem  3044  rmo3  3046  rmob  3047  ssrmof  3210  dfdisj2  3966  dffun9  5225  fncnv  5262