Definition df-reu 3366

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 3077). (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 3363	. 2 wff ∃!𝑥 ∈ 𝐴 𝜑
5	2	cv 1568	. . . . 5 class 𝑥
6	5, 3	wcel 2144	. . . 4 wff 𝑥 ∈ 𝐴
7	6, 1	wa 401	. . 3 wff (𝑥 ∈ 𝐴 ∧ 𝜑)
8	7, 2	weu 2593	. 2 wff ∃!𝑥(𝑥 ∈ 𝐴 ∧ 𝜑)
9	4, 8	wb 209	1 wff (∃!𝑥 ∈ 𝐴 𝜑 ↔ ∃!𝑥(𝑥 ∈ 𝐴 ∧ 𝜑))

This definition is used by:  reu5  3367  reubiia  3372  reubidva  3379  reueubd  3382  rmo5  3383  cbvreuvw  3387  reubida  3389  nfreu1  3393  nfreuw  3395  reueqbidv  3401  cbvreu  3404  nfreud  3409  reuv  3478  reurab  3658  reu2  3682  reu6  3683  reu3  3684  2reuswap  3703  2reuswap2  3704  2reu5lem1  3712  cbvreucsf  3890  reuun2  4270  reuss2  4271  reupick  4274  reupick3  4275  euelss  4277  reusn  4687  rabsneu  4689  reusv2lem4  5362  reusv2lem5  5363  reuhypd  5380  funcnv3  6610  feu  6758  dff4  7101  f1ompt  7111  fsn  7136  riotauni  7383  riotacl2  7393  riota1  7398  riota1a  7399  riota2df  7400  snriota  7410  riotaund  7416  aceq1  10196  dfac2b  10209  nqerf  11015  zmin  13071  climreu  15723  divalglem10  16572  divalgb  16574  uptx  23944  txcn  23945  q1peqb  26474  axcontlem2  29543  edgnbusgreu  29948  nbusgredgeu0  29949  frgr3vlem2  30875  3vfriswmgrlem  30878  frgrncvvdeqlem2  30901  adjeu  32491  reuxfrdf  33129  rmoxfrd  33131  reueqi  37020  reueqbii  37021  cbvreuvw2  37060  cbvreudavw  37084  cbvreudavw2  37115  neibastop3  37192  cbvreud  38339  poimirlem25  38606  poimirlem27  38608  dfsuccl4  39449  fsuppind  43661  onsucf1olem  44314  pairreueq  48634  prprsprreu  48643  prprreueq  48644  reutru  49956  dfralseu2  50961