Definition df-rmo 3369

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 3081). (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 3368	. 2 wff ∃*𝑥 ∈ 𝐴 𝜑
5	2	cv 1569	. . . . 5 class 𝑥
6	5, 3	wcel 2147	. . . 4 wff 𝑥 ∈ 𝐴
7	6, 1	wa 401	. . 3 wff (𝑥 ∈ 𝐴 ∧ 𝜑)
8	7, 2	wmo 2565	. 2 wff ∃*𝑥(𝑥 ∈ 𝐴 ∧ 𝜑)
9	4, 8	wb 209	1 wff (∃*𝑥 ∈ 𝐴 𝜑 ↔ ∃*𝑥(𝑥 ∈ 𝐴 ∧ 𝜑))

This definition is used by:  reu5  3371  mormo  3374  rmobiia  3375  rmobidva  3382  rmo5  3387  cbvrmovw  3390  rmobida  3392  cbvrmow  3394  nfrmo1  3396  nfrmow  3398  rmoeq1  3400  rmoeq1f  3406  nfrmod  3412  nfrmo  3414  rmov  3483  rmo4  3691  rmo3f  3695  rmoeq  3699  rmoan  3700  rmoim  3701  rmoimi2  3704  2reuswap  3707  2reu5lem2  3717  2rmoswap  3722  rmo2  3838  rmo3  3840  rmob  3841  rmob2  3844  rmoanim  3846  ssrmof  3981  dfdisj2  5075  rmorabex  5432  dffun9  6586  fncnv  6632  funcnvmpt  7015  iunmapdisj  10126  brdom4  10633  enqeq  11043  2ndcdisj  23802  2ndcdisj2  23803  pjhtheu  32023  pjpreeq  32027  cnlnadjeui  32706  reuxfrdf  33156  rmoxfrd  33158  rmoun  33159  rmounid  33160  cbvdisjf  33234  rmoeqi  37153  rmoeqbii  37154  rmoeqbidv  37179  disjeq12dv  37181  cbvrmovw2  37194  cbvrmodavw  37218  cbvrmodavw2  37249  nrmo  37375  alrmomorn  39481  alrmomodm  39482  dfeldisj4  39935  disjres  39967  cdleme0moN  41473  onsucf1olem  44462  tfsconcatlem  44528  modelaxreplem2  46162  rmotru  50116