Definition df-rmo 3114

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 3111). (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 3109	. 2 wff ∃*𝑥 ∈ 𝐴 𝜑
5	2	cv 1537	. . . . 5 class 𝑥
6	5, 3	wcel 2111	. . . 4 wff 𝑥 ∈ 𝐴
7	6, 1	wa 399	. . 3 wff (𝑥 ∈ 𝐴 ∧ 𝜑)
8	7, 2	wmo 2596	. 2 wff ∃*𝑥(𝑥 ∈ 𝐴 ∧ 𝜑)
9	4, 8	wb 209	1 wff (∃*𝑥 ∈ 𝐴 𝜑 ↔ ∃*𝑥(𝑥 ∈ 𝐴 ∧ 𝜑))

This definition is referenced by:  rmoanid  3287  nfrmo1  3324  nfrmod  3326  nfrmow  3328  nfrmo  3330  rmobida  3345  rmobiia  3348  rmoeq1f  3353  rmoeq1  3361  mormo  3374  reu5  3375  rmo5  3379  cbvrmow  3390  rmov  3469  rmo4  3669  rmo3f  3673  rmoeq  3677  rmoan  3678  rmoim  3679  rmoimi2  3682  2reuswap  3685  2reu5lem2  3695  2rmoswap  3700  rmo2  3816  rmo3  3818  rmob  3819  rmob2  3821  rmoanim  3823  ssrmof  3980  dfdisj2  4997  rmorabex  5317  dffun9  6353  fncnv  6397  iunmapdisj  9434  brdom4  9941  enqeq  10345  2ndcdisj  22061  2ndcdisj2  22062  pjhtheu  29177  pjpreeq  29181  cnlnadjeui  29860  reuxfrdf  30262  rmoxfrd  30264  rmoun  30265  rmounid  30266  cbvdisjf  30334  funcnvmpt  30430  nrmo  33871  alrmomorn  35772  alrmomodm  35773  dfeldisj4  36113  cdleme0moN  37521