Definition df-reu 3370

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 3079). (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 3367	. 2 wff ∃!𝑥 ∈ 𝐴 𝜑
5	2	cv 1561	. . . . 5 class 𝑥
6	5, 3	wcel 2144	. . . 4 wff 𝑥 ∈ 𝐴
7	6, 1	wa 399	. . 3 wff (𝑥 ∈ 𝐴 ∧ 𝜑)
8	7, 2	weu 2597	. 2 wff ∃!𝑥(𝑥 ∈ 𝐴 ∧ 𝜑)
9	4, 8	wb 208	1 wff (∃!𝑥 ∈ 𝐴 𝜑 ↔ ∃!𝑥(𝑥 ∈ 𝐴 ∧ 𝜑))

This definition is referenced by:  reu5  3371  reubiia  3376  reubidva  3383  reueubd  3386  rmo5  3387  cbvreuvw  3391  reubida  3393  nfreu1  3397  nfreuw  3399  reueqbidv  3405  cbvreu  3408  nfreud  3413  reuv  3484  reurab  3666  reu2  3690  reu6  3691  reu3  3692  2reuswap  3711  2reuswap2  3712  2reu5lem1  3720  cbvreucsf  3898  reuun2  4279  reuss2  4280  reupick  4283  reupick3  4284  euelss  4286  reusn  4688  rabsneu  4690  reusv2lem4  5360  reusv2lem5  5361  reuhypd  5378  funcnv3  6593  feu  6742  dff4  7084  f1ompt  7094  fsn  7119  riotauni  7361  riotacl2  7371  riota1  7376  riota1a  7377  riota2df  7378  snriota  7388  riotaund  7394  aceq1  10075  dfac2b  10089  nqerf  10890  zmin  12947  climreu  15585  divalglem10  16438  divalgb  16440  uptx  23687  txcn  23688  q1peqb  26218  axcontlem2  29168  edgnbusgreu  29570  nbusgredgeu0  29571  frgr3vlem2  30478  3vfriswmgrlem  30481  frgrncvvdeqlem2  30504  adjeu  32094  reuxfrdf  32692  rmoxfrd  32694  reueqi  36554  reueqbii  36555  cbvreuvw2  36594  cbvreudavw  36618  cbvreudavw2  36649  neibastop3  36727  cbvreud  37872  poimirlem25  38149  poimirlem27  38151  dfsuccl4  38978  fsuppind  43177  onsucf1olem  43852  pairreueq  48121  prprsprreu  48130  prprreueq  48131  reutru  49430