Definition df-rmo 3359

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 3052). (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 3358	. 2 wff ∃*𝑥 ∈ 𝐴 𝜑
5	2	cv 1539	. . . . 5 class 𝑥
6	5, 3	wcel 2108	. . . 4 wff 𝑥 ∈ 𝐴
7	6, 1	wa 395	. . 3 wff (𝑥 ∈ 𝐴 ∧ 𝜑)
8	7, 2	wmo 2537	. 2 wff ∃*𝑥(𝑥 ∈ 𝐴 ∧ 𝜑)
9	4, 8	wb 206	1 wff (∃*𝑥 ∈ 𝐴 𝜑 ↔ ∃*𝑥(𝑥 ∈ 𝐴 ∧ 𝜑))

This definition is referenced by:  reu5  3361  mormo  3364  rmobiia  3365  rmoanidOLD  3371  rmobidva  3374  rmo5  3379  cbvrmovw  3382  rmobida  3385  cbvrmow  3388  nfrmo1  3390  nfrmow  3392  rmoeq1  3395  rmoeq1OLD  3397  rmoeq1f  3403  nfrmowOLD  3406  nfrmod  3411  nfrmo  3413  rmov  3490  rmo4  3713  rmo3f  3717  rmoeq  3721  rmoan  3722  rmoim  3723  rmoimi2  3726  2reuswap  3729  2reu5lem2  3739  2rmoswap  3744  rmo2  3862  rmo3  3864  rmob  3865  rmob2  3867  rmoanim  3869  ssrmof  4026  dfdisj2  5088  rmorabex  5435  dffun9  6564  fncnv  6608  iunmapdisj  10035  brdom4  10542  enqeq  10946  2ndcdisj  23392  2ndcdisj2  23393  pjhtheu  31321  pjpreeq  31325  cnlnadjeui  32004  reuxfrdf  32418  rmoxfrd  32420  rmoun  32421  rmounid  32422  cbvdisjf  32498  funcnvmpt  32591  rmoeqi  36151  rmoeqbii  36152  rmoeqbidv  36177  disjeq12dv  36179  cbvrmovw2  36192  cbvrmodavw  36216  cbvrmodavw2  36247  nrmo  36374  alrmomorn  38322  alrmomodm  38323  dfeldisj4  38684  disjres  38708  cdleme0moN  40190  onsucf1olem  43241  tfsconcatlem  43307  modelaxreplem2  44952  rmotru  48730