Definition df-rmo 3374

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 3060). (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 3373	. 2 wff ∃*𝑥 ∈ 𝐴 𝜑
5	2	cv 1538	. . . . 5 class 𝑥
6	5, 3	wcel 2104	. . . 4 wff 𝑥 ∈ 𝐴
7	6, 1	wa 394	. . 3 wff (𝑥 ∈ 𝐴 ∧ 𝜑)
8	7, 2	wmo 2530	. 2 wff ∃*𝑥(𝑥 ∈ 𝐴 ∧ 𝜑)
9	4, 8	wb 205	1 wff (∃*𝑥 ∈ 𝐴 𝜑 ↔ ∃*𝑥(𝑥 ∈ 𝐴 ∧ 𝜑))

This definition is referenced by:  reu5  3376  mormo  3379  rmobiia  3380  rmoanidOLD  3386  rmobidva  3389  rmo5  3394  cbvrmovw  3397  rmobida  3400  cbvrmow  3403  nfrmo1  3405  nfrmow  3407  rmoeq1  3412  rmoeq1OLD  3414  rmoeq1f  3418  nfrmowOLD  3421  nfrmod  3426  nfrmo  3428  rmov  3500  rmo4  3725  rmo3f  3729  rmoeq  3733  rmoan  3734  rmoim  3735  rmoimi2  3738  2reuswap  3741  2reu5lem2  3751  2rmoswap  3756  rmo2  3880  rmo3  3882  rmob  3883  rmob2  3885  rmoanim  3887  ssrmof  4048  dfdisj2  5114  rmorabex  5459  dffun9  6576  fncnv  6620  iunmapdisj  10020  brdom4  10527  enqeq  10931  2ndcdisj  23180  2ndcdisj2  23181  pjhtheu  30914  pjpreeq  30918  cnlnadjeui  31597  reuxfrdf  31998  rmoxfrd  32000  rmoun  32001  rmounid  32002  cbvdisjf  32069  funcnvmpt  32159  nrmo  35598  alrmomorn  37530  alrmomodm  37531  dfeldisj4  37893  disjres  37917  cdleme0moN  39399  onsucf1olem  42322  tfsconcatlem  42388  rmotru  47576