Definition df-reu 3346

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 3045). (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 3343	. 2 wff ∃!𝑥 ∈ 𝐴 𝜑
5	2	cv 1539	. . . . 5 class 𝑥
6	5, 3	wcel 2109	. . . 4 wff 𝑥 ∈ 𝐴
7	6, 1	wa 395	. . 3 wff (𝑥 ∈ 𝐴 ∧ 𝜑)
8	7, 2	weu 2561	. 2 wff ∃!𝑥(𝑥 ∈ 𝐴 ∧ 𝜑)
9	4, 8	wb 206	1 wff (∃!𝑥 ∈ 𝐴 𝜑 ↔ ∃!𝑥(𝑥 ∈ 𝐴 ∧ 𝜑))

This definition is referenced by:  reu5  3347  reubiia  3352  reuanidOLD  3358  reubidva  3361  reueubd  3364  rmo5  3365  cbvreuvw  3369  reubida  3371  nfreu1  3375  nfreuw  3377  reueq1OLD  3381  reueqbidv  3385  cbvreu  3388  nfreud  3393  reuv  3467  reurab  3663  reu2  3687  reu6  3688  reu3  3689  2reuswap  3708  2reuswap2  3709  2reu5lem1  3717  cbvreucsf  3897  reuun2  4278  reuss2  4279  reupick  4282  reupick3  4283  euelss  4285  reusn  4681  rabsneu  4683  reusv2lem4  5343  reusv2lem5  5344  reuhypd  5361  funcnv3  6556  feu  6704  dff4  7039  f1ompt  7049  fsn  7073  riotauni  7316  riotacl2  7326  riota1  7331  riota1a  7332  riota2df  7333  snriota  7343  riotaund  7349  aceq1  10030  dfac2b  10044  nqerf  10843  zmin  12863  climreu  15481  divalglem10  16331  divalgb  16333  uptx  23528  txcn  23529  q1peqb  26077  axcontlem2  28928  edgnbusgreu  29330  nbusgredgeu0  29331  frgr3vlem2  30236  3vfriswmgrlem  30239  frgrncvvdeqlem2  30262  adjeu  31851  reuxfrdf  32453  rmoxfrd  32455  reueqi  36162  reueqbii  36163  cbvreuvw2  36202  cbvreudavw  36226  cbvreudavw2  36257  neibastop3  36335  cbvreud  37346  poimirlem25  37624  poimirlem27  37626  fsuppind  42563  onsucf1olem  43243  pairreueq  47495  prprsprreu  47504  prprreueq  47505  reutru  48789