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  3726  rmo3f  3730  rmoeq  3734  rmoan  3735  rmoim  3736  rmoimi2  3739  2reuswap  3742  2reu5lem2  3752  2rmoswap  3757  rmo2  3881  rmo3  3883  rmob  3884  rmob2  3886  rmoanim  3888  ssrmof  4049  dfdisj2  5115  rmorabex  5460  dffun9  6575  fncnv  6619  iunmapdisj  10015  brdom4  10522  enqeq  10926  2ndcdisj  22952  2ndcdisj2  22953  pjhtheu  30635  pjpreeq  30639  cnlnadjeui  31318  reuxfrdf  31719  rmoxfrd  31721  rmoun  31722  rmounid  31723  cbvdisjf  31790  funcnvmpt  31880  nrmo  35284  alrmomorn  37216  alrmomodm  37217  dfeldisj4  37579  disjres  37603  cdleme0moN  39085  onsucf1olem  42006  tfsconcatlem  42072  rmotru  47443