Definition df-rmo 2356

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

This definition is referenced by:  nfrmo1  2526  rmobida  2540  rmobiia  2543  rmoeq1f  2548  mormo  2565  reu5  2566  rmo5  2569  rmov  2619  rmo4  2785  rmoan  2790  rmoim  2791  rmoimi2  2793  2reuswapdc  2794  2rmorex  2796  rmo2ilem  2903  rmo3  2905  rmob  2906  dfdisj2  3768  dffun9  4950  fncnv  4985