Definition df-rmo 2518

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

This definition is referenced by:  nfrmo1  2706  cbvrmow  2716  rmobida  2721  rmobiia  2724  rmoeq1f  2729  mormo  2750  reu5  2751  rmo5  2754  rmov  2823  rmo4  2999  rmo3f  3003  rmoan  3006  rmoim  3007  rmoimi2  3009  2reuswapdc  3010  2rmorex  3012  rmo2ilem  3122  rmo3  3124  rmob  3125  ssrmof  3290  dfdisj2  4066  dffun9  5355  fncnv  5396