Definition df-rmo 2491

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

This definition is referenced by:  nfrmo1  2678  rmobida  2692  rmobiia  2695  rmoeq1f  2700  mormo  2721  reu5  2722  rmo5  2725  rmov  2791  rmo4  2965  rmo3f  2969  rmoan  2972  rmoim  2973  rmoimi2  2975  2reuswapdc  2976  2rmorex  2978  rmo2ilem  3087  rmo3  3089  rmob  3090  ssrmof  3255  dfdisj2  4022  dffun9  5297  fncnv  5334