Definition df-rmo 2949

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 2944	. 2 wff ∃*𝑥 ∈ 𝐴 𝜑
5	2	cv 1522	. . . . 5 class 𝑥
6	5, 3	wcel 2030	. . . 4 wff 𝑥 ∈ 𝐴
7	6, 1	wa 383	. . 3 wff (𝑥 ∈ 𝐴 ∧ 𝜑)
8	7, 2	wmo 2499	. 2 wff ∃*𝑥(𝑥 ∈ 𝐴 ∧ 𝜑)
9	4, 8	wb 196	1 wff (∃*𝑥 ∈ 𝐴 𝜑 ↔ ∃*𝑥(𝑥 ∈ 𝐴 ∧ 𝜑))

This definition is referenced by:  nfrmo1  3140  nfrmod  3142  nfrmo  3144  rmobida  3159  rmobiia  3162  rmoeq1f  3167  mormo  3188  reu5  3189  rmo5  3192  rmov  3253  rmo4  3432  rmoeq  3438  rmoan  3439  rmoim  3440  rmoimi2  3442  2reuswap  3443  2reu5lem2  3447  rmo2  3559  rmo3  3561  rmob  3562  rmob2  3564  dfdisj2  4654  reuxfr2d  4921  rmorabex  4958  dffun9  5955  fncnv  6000  iunmapdisj  8884  brdom4  9390  enqeq  9794  2ndcdisj  21307  2ndcdisj2  21308  pjhtheu  28381  pjpreeq  28385  cnlnadjeui  29064  rmoxfrd  29460  ssrmo  29461  rmo3f  29462  cbvdisjf  29511  funcnvmpt  29596  alrmomorn  34263  alrmomodm  34264  cdleme0moN  35830  2rmoswap  41505