Definition df-rmo 3346

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 3056). (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 3345	. 2 wff ∃*𝑥 ∈ 𝐴 𝜑
5	2	cv 1547	. . . . 5 class 𝑥
6	5, 3	wcel 2121	. . . 4 wff 𝑥 ∈ 𝐴
7	6, 1	wa 397	. . 3 wff (𝑥 ∈ 𝐴 ∧ 𝜑)
8	7, 2	wmo 2543	. 2 wff ∃*𝑥(𝑥 ∈ 𝐴 ∧ 𝜑)
9	4, 8	wb 208	1 wff (∃*𝑥 ∈ 𝐴 𝜑 ↔ ∃*𝑥(𝑥 ∈ 𝐴 ∧ 𝜑))

This definition is referenced by:  reu5  3348  mormo  3351  rmobiia  3352  rmobidva  3359  rmo5  3364  cbvrmovw  3367  rmobida  3369  cbvrmow  3371  nfrmo1  3373  nfrmow  3375  rmoeq1  3377  rmoeq1f  3383  nfrmod  3389  nfrmo  3391  rmov  3462  rmo4  3672  rmo3f  3676  rmoeq  3680  rmoan  3681  rmoim  3682  rmoimi2  3685  2reuswap  3688  2reu5lem2  3698  2rmoswap  3703  rmo2  3820  rmo3  3822  rmob  3823  rmob2  3825  rmoanim  3827  ssrmof  3984  dfdisj2  5043  rmorabex  5401  dffun9  6517  fncnv  6561  funcnvmpt  6940  iunmapdisj  9940  brdom4  10448  enqeq  10853  2ndcdisj  23442  2ndcdisj2  23443  pjhtheu  31485  pjpreeq  31489  cnlnadjeui  32168  reuxfrdf  32580  rmoxfrd  32582  rmoun  32583  rmounid  32584  cbvdisjf  32662  rmoeqi  36428  rmoeqbii  36429  rmoeqbidv  36454  disjeq12dv  36456  cbvrmovw2  36469  cbvrmodavw  36493  cbvrmodavw2  36524  nrmo  36651  alrmomorn  38738  alrmomodm  38739  dfeldisj4  39192  disjres  39224  cdleme0moN  40730  onsucf1olem  43728  tfsconcatlem  43794  modelaxreplem2  45436  rmotru  49305