Definition df-rmo 3111

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 3106	. 2 wff ∃*𝑥 ∈ 𝐴 𝜑
5	2	cv 1636	. . . . 5 class 𝑥
6	5, 3	wcel 2157	. . . 4 wff 𝑥 ∈ 𝐴
7	6, 1	wa 384	. . 3 wff (𝑥 ∈ 𝐴 ∧ 𝜑)
8	7, 2	wmo 2633	. 2 wff ∃*𝑥(𝑥 ∈ 𝐴 ∧ 𝜑)
9	4, 8	wb 197	1 wff (∃*𝑥 ∈ 𝐴 𝜑 ↔ ∃*𝑥(𝑥 ∈ 𝐴 ∧ 𝜑))

This definition is referenced by:  rmoanid  3116  nfrmo1  3306  nfrmod  3308  nfrmo  3310  rmobida  3325  rmobiia  3328  rmoeq1f  3333  mormo  3354  reu5  3355  rmo5  3358  rmov  3423  rmo4  3604  rmoeq  3610  rmoan  3611  rmoim  3612  rmoimi2  3614  2reuswap  3615  2reu5lem2  3619  rmo2  3728  rmo3  3730  rmob  3731  rmob2  3733  dfdisj2  4821  reuxfr2d  5095  rmorabex  5125  dffun9  6133  fncnv  6176  iunmapdisj  9132  brdom4  9640  enqeq  10044  2ndcdisj  21477  2ndcdisj2  21478  pjhtheu  28587  pjpreeq  28591  cnlnadjeui  29270  rmoxfrd  29665  ssrmo  29666  rmo3f  29667  cbvdisjf  29716  funcnvmpt  29801  alrmomorn  34438  alrmomodm  34439  cdleme0moN  36007  2rmoswap  41697