Definition df-rmo 3365

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

This definition is used by:  reu5  3367  mormo  3370  rmobiia  3371  rmobidva  3378  rmo5  3383  cbvrmovw  3386  rmobida  3388  cbvrmow  3390  nfrmo1  3392  nfrmow  3394  rmoeq1  3396  rmoeq1f  3402  nfrmod  3408  nfrmo  3410  rmov  3479  rmo4  3687  rmo3f  3691  rmoeq  3695  rmoan  3696  rmoim  3697  rmoimi2  3700  2reuswap  3703  2reu5lem2  3713  2rmoswap  3718  rmo2  3833  rmo3  3835  rmob  3836  rmob2  3839  rmoanim  3841  ssrmof  3998  dfdisj2  5071  rmorabex  5427  dffun9  6557  fncnv  6601  funcnvmpt  6983  iunmapdisj  10073  brdom4  10580  enqeq  10990  2ndcdisj  23736  2ndcdisj2  23737  pjhtheu  31929  pjpreeq  31933  cnlnadjeui  32612  reuxfrdf  33020  rmoxfrd  33022  rmoun  33023  rmounid  33024  cbvdisjf  33098  rmoeqi  36898  rmoeqbii  36899  rmoeqbidv  36924  disjeq12dv  36926  cbvrmovw2  36939  cbvrmodavw  36963  cbvrmodavw2  36994  nrmo  37120  alrmomorn  39210  alrmomodm  39211  dfeldisj4  39664  disjres  39696  cdleme0moN  41202  onsucf1olem  44215  tfsconcatlem  44281  modelaxreplem2  45906  rmotru  49835