Definition df-rmo 3364

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 3052). (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 3363	. 2 wff ∃*𝑥 ∈ 𝐴 𝜑
5	2	cv 1533	. . . . 5 class 𝑥
6	5, 3	wcel 2099	. . . 4 wff 𝑥 ∈ 𝐴
7	6, 1	wa 394	. . 3 wff (𝑥 ∈ 𝐴 ∧ 𝜑)
8	7, 2	wmo 2527	. 2 wff ∃*𝑥(𝑥 ∈ 𝐴 ∧ 𝜑)
9	4, 8	wb 205	1 wff (∃*𝑥 ∈ 𝐴 𝜑 ↔ ∃*𝑥(𝑥 ∈ 𝐴 ∧ 𝜑))

This definition is referenced by:  reu5  3366  mormo  3369  rmobiia  3370  rmoanidOLD  3376  rmobidva  3379  rmo5  3384  cbvrmovw  3387  rmobida  3390  cbvrmow  3393  nfrmo1  3395  nfrmow  3397  rmoeq1  3401  rmoeq1OLD  3403  rmoeq1f  3407  nfrmowOLD  3410  nfrmod  3415  nfrmo  3417  rmov  3492  rmo4  3724  rmo3f  3728  rmoeq  3732  rmoan  3733  rmoim  3734  rmoimi2  3737  2reuswap  3740  2reu5lem2  3750  2rmoswap  3755  rmo2  3880  rmo3  3882  rmob  3883  rmob2  3885  rmoanim  3887  ssrmof  4047  dfdisj2  5120  rmorabex  5466  dffun9  6588  fncnv  6632  iunmapdisj  10066  brdom4  10573  enqeq  10977  2ndcdisj  23451  2ndcdisj2  23452  pjhtheu  31327  pjpreeq  31331  cnlnadjeui  32010  reuxfrdf  32419  rmoxfrd  32421  rmoun  32422  rmounid  32423  cbvdisjf  32491  funcnvmpt  32584  nrmo  36122  alrmomorn  38056  alrmomodm  38057  dfeldisj4  38418  disjres  38442  cdleme0moN  39924  onsucf1olem  42936  tfsconcatlem  43002  rmotru  48190