Definition df-rmo 2516

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

This definition is referenced by:  nfrmo1  2704  cbvrmow  2714  rmobida  2719  rmobiia  2722  rmoeq1f  2727  mormo  2748  reu5  2749  rmo5  2752  rmov  2821  rmo4  2997  rmo3f  3001  rmoan  3004  rmoim  3005  rmoimi2  3007  2reuswapdc  3008  2rmorex  3010  rmo2ilem  3120  rmo3  3122  rmob  3123  ssrmof  3288  dfdisj2  4064  dffun9  5353  fncnv  5393