Definition df-rmo 2363

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 2358	. 2 wff ∃*𝑥 ∈ 𝐴 𝜑
5	2	cv 1286	. . . . 5 class 𝑥
6	5, 3	wcel 1436	. . . 4 wff 𝑥 ∈ 𝐴
7	6, 1	wa 102	. . 3 wff (𝑥 ∈ 𝐴 ∧ 𝜑)
8	7, 2	wmo 1946	. 2 wff ∃*𝑥(𝑥 ∈ 𝐴 ∧ 𝜑)
9	4, 8	wb 103	1 wff (∃*𝑥 ∈ 𝐴 𝜑 ↔ ∃*𝑥(𝑥 ∈ 𝐴 ∧ 𝜑))

This definition is referenced by:  nfrmo1  2535  rmobida  2549  rmobiia  2552  rmoeq1f  2557  mormo  2574  reu5  2575  rmo5  2578  rmov  2633  rmo4  2799  rmoan  2804  rmoim  2805  rmoimi2  2807  2reuswapdc  2808  2rmorex  2810  rmo2ilem  2917  rmo3  2919  rmob  2920  dfdisj2  3805  dffun9  5011  fncnv  5047