Definition df-rmo 3348

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 3050). (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 3347	. 2 wff ∃*𝑥 ∈ 𝐴 𝜑
5	2	cv 1540	. . . . 5 class 𝑥
6	5, 3	wcel 2113	. . . 4 wff 𝑥 ∈ 𝐴
7	6, 1	wa 395	. . 3 wff (𝑥 ∈ 𝐴 ∧ 𝜑)
8	7, 2	wmo 2535	. 2 wff ∃*𝑥(𝑥 ∈ 𝐴 ∧ 𝜑)
9	4, 8	wb 206	1 wff (∃*𝑥 ∈ 𝐴 𝜑 ↔ ∃*𝑥(𝑥 ∈ 𝐴 ∧ 𝜑))

This definition is referenced by:  reu5  3350  mormo  3353  rmobiia  3354  rmobidva  3361  rmo5  3366  cbvrmovw  3369  rmobida  3371  cbvrmow  3373  nfrmo1  3375  nfrmow  3377  rmoeq1  3379  rmoeq1OLD  3381  rmoeq1f  3387  nfrmod  3393  nfrmo  3395  rmov  3468  rmo4  3686  rmo3f  3690  rmoeq  3694  rmoan  3695  rmoim  3696  rmoimi2  3699  2reuswap  3702  2reu5lem2  3712  2rmoswap  3717  rmo2  3835  rmo3  3837  rmob  3838  rmob2  3840  rmoanim  3842  ssrmof  3999  dfdisj2  5065  rmorabex  5406  dffun9  6519  fncnv  6563  iunmapdisj  9931  brdom4  10438  enqeq  10843  2ndcdisj  23398  2ndcdisj2  23399  pjhtheu  31418  pjpreeq  31422  cnlnadjeui  32101  reuxfrdf  32514  rmoxfrd  32516  rmoun  32517  rmounid  32518  cbvdisjf  32595  funcnvmpt  32694  rmoeqi  36330  rmoeqbii  36331  rmoeqbidv  36356  disjeq12dv  36358  cbvrmovw2  36371  cbvrmodavw  36395  cbvrmodavw2  36426  nrmo  36553  alrmomorn  38490  alrmomodm  38491  dfeldisj4  38918  disjres  38942  cdleme0moN  40424  onsucf1olem  43454  tfsconcatlem  43520  modelaxreplem2  45162  rmotru  48990