Definition df-reu 3378

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 3059). (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 3375	. 2 wff ∃!𝑥 ∈ 𝐴 𝜑
5	2	cv 1535	. . . . 5 class 𝑥
6	5, 3	wcel 2105	. . . 4 wff 𝑥 ∈ 𝐴
7	6, 1	wa 395	. . 3 wff (𝑥 ∈ 𝐴 ∧ 𝜑)
8	7, 2	weu 2565	. 2 wff ∃!𝑥(𝑥 ∈ 𝐴 ∧ 𝜑)
9	4, 8	wb 206	1 wff (∃!𝑥 ∈ 𝐴 𝜑 ↔ ∃!𝑥(𝑥 ∈ 𝐴 ∧ 𝜑))

This definition is referenced by:  reu5  3379  reubiia  3384  reuanidOLD  3390  reubidva  3393  reueubd  3396  rmo5  3397  cbvreuvw  3401  reubida  3404  nfreu1  3409  nfreuw  3411  cbvreuwOLD  3412  reueq1OLD  3416  nfreuwOLD  3422  cbvreu  3424  nfreud  3429  reuv  3507  reurab  3709  reu2  3733  reu6  3734  reu3  3735  2reuswap  3754  2reuswap2  3755  2reu5lem1  3763  cbvreucsf  3954  reuun2  4330  reuss2  4331  reupick  4334  reupick3  4335  euelss  4337  reusn  4731  rabsneu  4733  reusv2lem4  5406  reusv2lem5  5407  reuhypd  5424  funcnv3  6637  feu  6784  dff4  7120  f1ompt  7130  fsn  7154  riotauni  7393  riotacl2  7403  riota1  7408  riota1a  7409  riota2df  7410  snriota  7420  riotaund  7426  aceq1  10154  dfac2b  10168  nqerf  10967  zmin  12983  climreu  15588  divalglem10  16435  divalgb  16437  uptx  23648  txcn  23649  q1peqb  26209  axcontlem2  28994  edgnbusgreu  29398  nbusgredgeu0  29399  frgr3vlem2  30302  3vfriswmgrlem  30305  frgrncvvdeqlem2  30328  adjeu  31917  reuxfrdf  32518  rmoxfrd  32520  reueqi  36170  reueqbii  36171  reueqbidv  36195  cbvreuvw2  36211  cbvreudavw  36235  cbvreudavw2  36266  neibastop3  36344  cbvreud  37355  poimirlem25  37631  poimirlem27  37633  fsuppind  42576  onsucf1olem  43259  pairreueq  47434  prprsprreu  47443  prprreueq  47444  reutru  48652