Definition df-reu 3365

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 3052). (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 3362	. 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	weu 2557	. 2 wff ∃!𝑥(𝑥 ∈ 𝐴 ∧ 𝜑)
9	4, 8	wb 205	1 wff (∃!𝑥 ∈ 𝐴 𝜑 ↔ ∃!𝑥(𝑥 ∈ 𝐴 ∧ 𝜑))

This definition is referenced by:  reu5  3366  reubiia  3371  reuanidOLD  3377  reubidva  3380  reueubd  3383  rmo5  3384  cbvreuvw  3388  reubida  3391  nfreu1  3396  nfreuw  3398  cbvreuwOLD  3399  reueq1OLD  3404  nfreuwOLD  3409  cbvreu  3411  nfreud  3416  reuv  3491  reurab  3694  reu2  3718  reu6  3719  reu3  3720  2reuswap  3739  2reuswap2  3740  2reu5lem1  3748  cbvreucsf  3938  reuun2  4314  reuss2  4315  reupick  4318  reupick3  4319  euelss  4321  reusn  4726  rabsneu  4728  reusv2lem4  5397  reusv2lem5  5398  reuhypd  5415  funcnv3  6621  feu  6770  dff4  7107  f1ompt  7117  fsn  7141  riotauni  7378  riotacl2  7389  riota1  7394  riota1a  7395  riota2df  7396  snriota  7406  riotaund  7412  aceq1  10153  dfac2b  10166  nqerf  10964  zmin  12974  climreu  15553  divalglem10  16399  divalgb  16401  uptx  23617  txcn  23618  q1peqb  26180  axcontlem2  28896  edgnbusgreu  29300  nbusgredgeu0  29301  frgr3vlem2  30204  3vfriswmgrlem  30207  frgrncvvdeqlem2  30230  adjeu  31819  reuxfrdf  32416  rmoxfrd  32418  neibastop3  36087  cbvreud  37093  poimirlem25  37359  poimirlem27  37361  fsuppind  42280  onsucf1olem  42973  pairreueq  47118  prprsprreu  47127  prprreueq  47128  reutru  48227