Definition df-reu 3072

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 3069). (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 3066	. 2 wff ∃!𝑥 ∈ 𝐴 𝜑
5	2	cv 1538	. . . . 5 class 𝑥
6	5, 3	wcel 2106	. . . 4 wff 𝑥 ∈ 𝐴
7	6, 1	wa 396	. . 3 wff (𝑥 ∈ 𝐴 ∧ 𝜑)
8	7, 2	weu 2568	. 2 wff ∃!𝑥(𝑥 ∈ 𝐴 ∧ 𝜑)
9	4, 8	wb 205	1 wff (∃!𝑥 ∈ 𝐴 𝜑 ↔ ∃!𝑥(𝑥 ∈ 𝐴 ∧ 𝜑))

This definition is referenced by:  reuanid  3298  nfreu1  3300  nfreud  3302  nfreuw  3305  nfreuwOLD  3306  reubida  3321  reubidva  3322  reubiia  3324  reueq1f  3334  reueq1  3344  reu5  3361  rmo5  3365  reueubd  3367  cbvreuwOLD  3377  cbvreu  3381  cbvreuvw  3386  reuv  3458  reu2  3660  reu6  3661  reu3  3662  2reuswap  3681  2reuswap2  3682  2reu5lem1  3690  cbvreucsf  3879  reuun2  4248  reuss2  4249  reupick  4252  reupick3  4253  euelss  4255  reusn  4663  rabsneu  4665  reusv2lem4  5324  reusv2lem5  5325  reuhypd  5342  funcnv3  6504  feu  6650  dff4  6977  f1ompt  6985  fsn  7007  riotauni  7238  riotacl2  7249  riota1  7254  riota1a  7255  riota2df  7256  snriota  7266  riotaund  7272  aceq1  9873  dfac2b  9886  nqerf  10686  zmin  12684  climreu  15265  divalglem10  16111  divalgb  16113  uptx  22776  txcn  22777  q1peqb  25319  axcontlem2  27333  edgnbusgreu  27734  nbusgredgeu0  27735  frgr3vlem2  28638  3vfriswmgrlem  28641  frgrncvvdeqlem2  28664  adjeu  30251  reuxfrdf  30839  rmoxfrd  30841  reurab  33674  neibastop3  34551  cbvreud  35544  poimirlem25  35802  poimirlem27  35804  fsuppind  40279  pairreueq  44962  prprsprreu  44971  prprreueq  44972  reutru  46151