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 1568	. . . . 5 class 𝑥
6	5, 3	wcel 2144	. . . 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  3976  dfdisj2  5071  rmorabex  5427  dffun9  6569  fncnv  6613  funcnvmpt  6995  iunmapdisj  10102  brdom4  10609  enqeq  11019  2ndcdisj  23775  2ndcdisj2  23776  pjhtheu  31996  pjpreeq  32000  cnlnadjeui  32679  reuxfrdf  33129  rmoxfrd  33131  rmoun  33132  rmounid  33133  cbvdisjf  33207  rmoeqi  37018  rmoeqbii  37019  rmoeqbidv  37044  disjeq12dv  37046  cbvrmovw2  37059  cbvrmodavw  37083  cbvrmodavw2  37114  nrmo  37240  alrmomorn  39333  alrmomodm  39334  dfeldisj4  39787  disjres  39819  cdleme0moN  41325  onsucf1olem  44314  tfsconcatlem  44380  modelaxreplem2  46011  rmotru  49955