Definition df-rmo 3377

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 3063). (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 3376	. 2 wff ∃*𝑥 ∈ 𝐴 𝜑
5	2	cv 1541	. . . . 5 class 𝑥
6	5, 3	wcel 2107	. . . 4 wff 𝑥 ∈ 𝐴
7	6, 1	wa 397	. . 3 wff (𝑥 ∈ 𝐴 ∧ 𝜑)
8	7, 2	wmo 2533	. 2 wff ∃*𝑥(𝑥 ∈ 𝐴 ∧ 𝜑)
9	4, 8	wb 205	1 wff (∃*𝑥 ∈ 𝐴 𝜑 ↔ ∃*𝑥(𝑥 ∈ 𝐴 ∧ 𝜑))

This definition is referenced by:  reu5  3379  mormo  3382  rmobiia  3383  rmoanidOLD  3389  rmobidva  3392  rmo5  3397  cbvrmovw  3400  rmobida  3403  cbvrmow  3406  nfrmo1  3408  nfrmow  3410  rmoeq1  3415  rmoeq1OLD  3417  rmoeq1f  3421  nfrmowOLD  3424  nfrmod  3429  nfrmo  3431  rmov  3502  rmo4  3727  rmo3f  3731  rmoeq  3735  rmoan  3736  rmoim  3737  rmoimi2  3740  2reuswap  3743  2reu5lem2  3753  2rmoswap  3758  rmo2  3882  rmo3  3884  rmob  3885  rmob2  3887  rmoanim  3889  ssrmof  4050  dfdisj2  5116  rmorabex  5461  dffun9  6578  fncnv  6622  iunmapdisj  10018  brdom4  10525  enqeq  10929  2ndcdisj  22960  2ndcdisj2  22961  pjhtheu  30647  pjpreeq  30651  cnlnadjeui  31330  reuxfrdf  31731  rmoxfrd  31733  rmoun  31734  rmounid  31735  cbvdisjf  31802  funcnvmpt  31892  nrmo  35295  alrmomorn  37227  alrmomodm  37228  dfeldisj4  37590  disjres  37614  cdleme0moN  39096  onsucf1olem  42020  tfsconcatlem  42086  rmotru  47489