Definition df-rmo 2920

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 2915	. 2 wff ∃*𝑥 ∈ 𝐴 𝜑
5	2	cv 1482	. . . . 5 class 𝑥
6	5, 3	wcel 1990	. . . 4 wff 𝑥 ∈ 𝐴
7	6, 1	wa 384	. . 3 wff (𝑥 ∈ 𝐴 ∧ 𝜑)
8	7, 2	wmo 2471	. 2 wff ∃*𝑥(𝑥 ∈ 𝐴 ∧ 𝜑)
9	4, 8	wb 196	1 wff (∃*𝑥 ∈ 𝐴 𝜑 ↔ ∃*𝑥(𝑥 ∈ 𝐴 ∧ 𝜑))

This definition is referenced by:  nfrmo1  3111  nfrmod  3113  nfrmo  3115  rmobida  3129  rmobiia  3132  rmoeq1f  3137  mormo  3158  reu5  3159  rmo5  3162  rmov  3222  rmo4  3399  rmoeq  3405  rmoan  3406  rmoim  3407  rmoimi2  3409  2reuswap  3410  2reu5lem2  3414  rmo2  3526  rmo3  3528  rmob  3529  rmob2  3531  dfdisj2  4622  reuxfr2d  4891  rmorabex  4928  dffun9  5917  fncnv  5962  iunmapdisj  8846  brdom4  9352  enqeq  9756  2ndcdisj  21259  2ndcdisj2  21260  pjhtheu  28253  pjpreeq  28257  cnlnadjeui  28936  rmoxfrd  29333  ssrmo  29334  rmo3f  29335  cbvdisjf  29385  funcnvmpt  29468  alrmomo  34123  alrmomo2  34124  cdleme0moN  35512  2rmoswap  41184