Definition df-reu 3347

Description: Define restricted existential uniqueness.

Note: This notation is most often used to express that 𝜑 holds for exactly 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 exactly one 𝑥 fulfilling 𝜑 happens to be contained in the corresponding 𝐴(𝑥). This interpretation is rarely needed (see also df-ral 3056). (Contributed by NM, 22-Nov-1994.)

Assertion

Ref	Expression
df-reu	⊢ (∃!𝑥 ∈ 𝐴 𝜑 ↔ ∃!𝑥(𝑥 ∈ 𝐴 ∧ 𝜑))

Detailed syntax breakdown of Definition df-reu

Step	Hyp	Ref	Expression
1		wph	. . 3 wff 𝜑
2		vx	. . 3 setvar 𝑥
3		cA	. . 3 class 𝐴
4	1, 2, 3	wreu 3344	. 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	weu 2574	. 2 wff ∃!𝑥(𝑥 ∈ 𝐴 ∧ 𝜑)
9	4, 8	wb 208	1 wff (∃!𝑥 ∈ 𝐴 𝜑 ↔ ∃!𝑥(𝑥 ∈ 𝐴 ∧ 𝜑))

This definition is referenced by:  reu5  3348  reubiia  3353  reubidva  3360  reueubd  3363  rmo5  3364  cbvreuvw  3368  reubida  3370  nfreu1  3374  nfreuw  3376  reueqbidv  3382  cbvreu  3385  nfreud  3390  reuv  3461  reurab  3643  reu2  3667  reu6  3668  reu3  3669  2reuswap  3688  2reuswap2  3689  2reu5lem1  3697  cbvreucsf  3876  reuun2  4255  reuss2  4256  reupick  4259  reupick3  4260  euelss  4262  reusn  4661  rabsneu  4663  reusv2lem4  5332  reusv2lem5  5333  reuhypd  5350  funcnv3  6558  feu  6706  dff4  7045  f1ompt  7055  fsn  7080  riotauni  7322  riotacl2  7332  riota1  7337  riota1a  7338  riota2df  7339  snriota  7349  riotaund  7355  aceq1  10034  dfac2b  10048  nqerf  10849  zmin  12889  climreu  15513  divalglem10  16366  divalgb  16368  uptx  23611  txcn  23612  q1peqb  26142  axcontlem2  29054  edgnbusgreu  29456  nbusgredgeu0  29457  frgr3vlem2  30364  3vfriswmgrlem  30367  frgrncvvdeqlem2  30390  adjeu  31980  reuxfrdf  32580  rmoxfrd  32582  reueqi  36430  reueqbii  36431  cbvreuvw2  36470  cbvreudavw  36494  cbvreudavw2  36525  neibastop3  36603  cbvreud  37748  poimirlem25  38025  poimirlem27  38027  dfsuccl4  38854  fsuppind  43053  onsucf1olem  43728  pairreueq  47997  prprsprreu  48006  prprreueq  48007  reutru  49306