Definition df-reu 3352

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 3349	. 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  3353  reubiia  3358  reubidva  3365  reueubd  3368  rmo5  3369  cbvreuvw  3373  reubida  3375  nfreu1  3379  nfreuw  3381  reueq1OLD  3385  reueqbidv  3389  cbvreu  3392  nfreud  3397  reuv  3470  reurab  3660  reu2  3684  reu6  3685  reu3  3686  2reuswap  3705  2reuswap2  3706  2reu5lem1  3714  cbvreucsf  3894  reuun2  4278  reuss2  4279  reupick  4282  reupick3  4283  euelss  4285  reusn  4685  rabsneu  4687  reusv2lem4  5347  reusv2lem5  5348  reuhypd  5365  funcnv3  6563  feu  6711  dff4  7048  f1ompt  7058  fsn  7082  riotauni  7323  riotacl2  7333  riota1  7338  riota1a  7339  riota2df  7340  snriota  7350  riotaund  7356  aceq1  10031  dfac2b  10045  nqerf  10845  zmin  12861  climreu  15483  divalglem10  16333  divalgb  16335  uptx  23573  txcn  23574  q1peqb  26121  axcontlem2  29042  edgnbusgreu  29444  nbusgredgeu0  29445  frgr3vlem2  30353  3vfriswmgrlem  30356  frgrncvvdeqlem2  30379  adjeu  31968  reuxfrdf  32568  rmoxfrd  32570  reueqi  36385  reueqbii  36386  cbvreuvw2  36425  cbvreudavw  36449  cbvreudavw2  36480  neibastop3  36558  cbvreud  37580  poimirlem25  37848  poimirlem27  37850  dfsuccl4  38677  fsuppind  42900  onsucf1olem  43579  pairreueq  47823  prprsprreu  47832  prprreueq  47833  reutru  49116