Definition df-rmo 3366

Description: Define restricted "at most one". Note: This notation is most often used to express that 𝜑 holds for at most one element of a given class 𝐴. For this reading Ⅎ𝑥𝐴 is required, though, for example, asserted when 𝑥 and 𝐴 are disjoint.

Should instead 𝐴 depend on 𝑥, you rather assert at most one 𝑥 fulfilling 𝜑 happens to be contained in the corresponding 𝐴(𝑥). This interpretation is rarely needed (see also df-ral 3078). (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 3365	. 2 wff ∃*𝑥 ∈ 𝐴 𝜑
5	2	cv 1569	. . . . 5 class 𝑥
6	5, 3	wcel 2145	. . . 4 wff 𝑥 ∈ 𝐴
7	6, 1	wa 401	. . 3 wff (𝑥 ∈ 𝐴 ∧ 𝜑)
8	7, 2	wmo 2563	. 2 wff ∃*𝑥(𝑥 ∈ 𝐴 ∧ 𝜑)
9	4, 8	wb 209	1 wff (∃*𝑥 ∈ 𝐴 𝜑 ↔ ∃*𝑥(𝑥 ∈ 𝐴 ∧ 𝜑))

This definition is used by:  reu5  3368  mormo  3371  rmobiia  3372  rmobidva  3379  rmo5  3384  cbvrmovw  3387  rmobida  3389  cbvrmow  3391  nfrmo1  3393  nfrmow  3395  rmoeq1  3397  rmoeq1f  3403  nfrmod  3409  nfrmo  3411  rmov  3480  rmo4  3688  rmo3f  3692  rmoeq  3696  rmoan  3697  rmoim  3698  rmoimi2  3701  2reuswap  3704  2reu5lem2  3714  2rmoswap  3719  rmo2  3834  rmo3  3836  rmob  3837  rmob2  3840  rmoanim  3842  ssrmof  3999  dfdisj2  5072  rmorabex  5428  dffun9  6569  fncnv  6613  funcnvmpt  6995  iunmapdisj  10102  brdom4  10609  enqeq  11019  2ndcdisj  23775  2ndcdisj2  23776  pjhtheu  31996  pjpreeq  32000  cnlnadjeui  32679  reuxfrdf  33087  rmoxfrd  33089  rmoun  33090  rmounid  33091  cbvdisjf  33165  rmoeqi  36976  rmoeqbii  36977  rmoeqbidv  37002  disjeq12dv  37004  cbvrmovw2  37017  cbvrmodavw  37041  cbvrmodavw2  37072  nrmo  37198  alrmomorn  39290  alrmomodm  39291  dfeldisj4  39744  disjres  39776  cdleme0moN  41282  onsucf1olem  44271  tfsconcatlem  44337  modelaxreplem2  45968  rmotru  49912