Definition df-reu 3353

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 3053). (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 3350	. 2 wff ∃!𝑥 ∈ 𝐴 𝜑
5	2	cv 1541	. . . . 5 class 𝑥
6	5, 3	wcel 2114	. . . 4 wff 𝑥 ∈ 𝐴
7	6, 1	wa 395	. . 3 wff (𝑥 ∈ 𝐴 ∧ 𝜑)
8	7, 2	weu 2569	. 2 wff ∃!𝑥(𝑥 ∈ 𝐴 ∧ 𝜑)
9	4, 8	wb 206	1 wff (∃!𝑥 ∈ 𝐴 𝜑 ↔ ∃!𝑥(𝑥 ∈ 𝐴 ∧ 𝜑))

This definition is referenced by:  reu5  3354  reubiia  3359  reubidva  3366  reueubd  3369  rmo5  3370  cbvreuvw  3374  reubida  3376  nfreu1  3380  nfreuw  3382  reueq1OLD  3386  reueqbidv  3390  cbvreu  3393  nfreud  3398  reuv  3471  reurab  3661  reu2  3685  reu6  3686  reu3  3687  2reuswap  3706  2reuswap2  3707  2reu5lem1  3715  cbvreucsf  3895  reuun2  4279  reuss2  4280  reupick  4283  reupick3  4284  euelss  4286  reusn  4686  rabsneu  4688  reusv2lem4  5350  reusv2lem5  5351  reuhypd  5368  funcnv3  6572  feu  6720  dff4  7057  f1ompt  7067  fsn  7092  riotauni  7333  riotacl2  7343  riota1  7348  riota1a  7349  riota2df  7350  snriota  7360  riotaund  7366  aceq1  10041  dfac2b  10055  nqerf  10855  zmin  12871  climreu  15493  divalglem10  16343  divalgb  16345  uptx  23586  txcn  23587  q1peqb  26134  axcontlem2  29056  edgnbusgreu  29458  nbusgredgeu0  29459  frgr3vlem2  30367  3vfriswmgrlem  30370  frgrncvvdeqlem2  30393  adjeu  31983  reuxfrdf  32583  rmoxfrd  32585  reueqi  36411  reueqbii  36412  cbvreuvw2  36451  cbvreudavw  36475  cbvreudavw2  36506  neibastop3  36584  cbvreud  37655  poimirlem25  37925  poimirlem27  37927  dfsuccl4  38754  fsuppind  42977  onsucf1olem  43656  pairreueq  47899  prprsprreu  47908  prprreueq  47909  reutru  49192