Definition df-rmo 3367

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 3079). (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 3366	. 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 2564	. 2 wff ∃*𝑥(𝑥 ∈ 𝐴 ∧ 𝜑)
9	4, 8	wb 209	1 wff (∃*𝑥 ∈ 𝐴 𝜑 ↔ ∃*𝑥(𝑥 ∈ 𝐴 ∧ 𝜑))

This definition is used by:  reu5  3369  mormo  3372  rmobiia  3373  rmobidva  3380  rmo5  3385  cbvrmovw  3388  rmobida  3390  cbvrmow  3392  nfrmo1  3394  nfrmow  3396  rmoeq1  3398  rmoeq1f  3404  nfrmod  3410  nfrmo  3412  rmov  3482  rmo4  3691  rmo3f  3695  rmoeq  3699  rmoan  3700  rmoim  3701  rmoimi2  3704  2reuswap  3707  2reu5lem2  3717  2rmoswap  3722  rmo2  3837  rmo3  3839  rmob  3840  rmob2  3843  rmoanim  3845  ssrmof  4002  dfdisj2  5076  rmorabex  5439  dffun9  6566  fncnv  6610  funcnvmpt  6992  iunmapdisj  10029  brdom4  10536  enqeq  10946  2ndcdisj  23683  2ndcdisj2  23684  pjhtheu  31861  pjpreeq  31865  cnlnadjeui  32544  reuxfrdf  32952  rmoxfrd  32954  rmoun  32955  rmounid  32956  cbvdisjf  33031  rmoeqi  36794  rmoeqbii  36795  rmoeqbidv  36820  disjeq12dv  36822  cbvrmovw2  36835  cbvrmodavw  36859  cbvrmodavw2  36890  nrmo  37016  alrmomorn  39093  alrmomodm  39094  dfeldisj4  39547  disjres  39579  cdleme0moN  41085  onsucf1olem  44098  tfsconcatlem  44164  modelaxreplem2  45789  rmotru  49718