Definition df-rmo 2530

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

This definition is referenced by:  nfrmo1  2718  cbvrmow  2729  rmobida  2734  rmobiia  2737  rmoeq1f  2742  mormo  2763  reu5  2764  rmo5  2767  rmov  2836  rmo4  3012  rmo3f  3016  rmoan  3019  rmoim  3020  rmoimi2  3022  2reuswapdc  3023  2rmorex  3025  rmo2ilem  3135  rmo3  3137  rmob  3138  ssrmof  3303  dfdisj2  4089  dffun9  5383  fncnv  5424