Definition df-reu 3348

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 3049). (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 3345	. 2 wff ∃!𝑥 ∈ 𝐴 𝜑
5	2	cv 1540	. . . . 5 class 𝑥
6	5, 3	wcel 2113	. . . 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  3349  reubiia  3354  reubidva  3361  reueubd  3364  rmo5  3365  cbvreuvw  3369  reubida  3371  nfreu1  3375  nfreuw  3377  reueq1OLD  3381  reueqbidv  3385  cbvreu  3388  nfreud  3393  reuv  3466  reurab  3656  reu2  3680  reu6  3681  reu3  3682  2reuswap  3701  2reuswap2  3702  2reu5lem1  3710  cbvreucsf  3890  reuun2  4274  reuss2  4275  reupick  4278  reupick3  4279  euelss  4281  reusn  4679  rabsneu  4681  reusv2lem4  5341  reusv2lem5  5342  reuhypd  5359  funcnv3  6556  feu  6704  dff4  7040  f1ompt  7050  fsn  7074  riotauni  7315  riotacl2  7325  riota1  7330  riota1a  7331  riota2df  7332  snriota  7342  riotaund  7348  aceq1  10015  dfac2b  10029  nqerf  10828  zmin  12844  climreu  15465  divalglem10  16315  divalgb  16317  uptx  23541  txcn  23542  q1peqb  26089  axcontlem2  28945  edgnbusgreu  29347  nbusgredgeu0  29348  frgr3vlem2  30256  3vfriswmgrlem  30259  frgrncvvdeqlem2  30282  adjeu  31871  reuxfrdf  32472  rmoxfrd  32474  reueqi  36254  reueqbii  36255  cbvreuvw2  36294  cbvreudavw  36318  cbvreudavw2  36349  neibastop3  36427  cbvreud  37438  poimirlem25  37705  poimirlem27  37707  dfsuccl4  38507  fsuppind  42708  onsucf1olem  43387  pairreueq  47634  prprsprreu  47643  prprreueq  47644  reutru  48928