Definition df-reu 3341

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 3050). (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 3338	. 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 2567	. 2 wff ∃!𝑥(𝑥 ∈ 𝐴 ∧ 𝜑)
9	4, 8	wb 206	1 wff (∃!𝑥 ∈ 𝐴 𝜑 ↔ ∃!𝑥(𝑥 ∈ 𝐴 ∧ 𝜑))

This definition is referenced by:  reu5  3342  reubiia  3347  reubidva  3354  reueubd  3357  rmo5  3358  cbvreuvw  3362  reubida  3364  nfreu1  3368  nfreuw  3370  reueqbidv  3376  cbvreu  3379  nfreud  3384  reuv  3456  reurab  3644  reu2  3668  reu6  3669  reu3  3670  2reuswap  3689  2reuswap2  3690  2reu5lem1  3698  cbvreucsf  3877  reuun2  4255  reuss2  4256  reupick  4259  reupick3  4260  euelss  4262  reusn  4661  rabsneu  4663  reusv2lem4  5332  reusv2lem5  5333  reuhypd  5350  funcnv3  6557  feu  6705  dff4  7042  f1ompt  7052  fsn  7077  riotauni  7319  riotacl2  7329  riota1  7334  riota1a  7335  riota2df  7336  snriota  7346  riotaund  7352  aceq1  10028  dfac2b  10042  nqerf  10842  zmin  12883  climreu  15507  divalglem10  16360  divalgb  16362  uptx  23578  txcn  23579  q1peqb  26109  axcontlem2  29022  edgnbusgreu  29424  nbusgredgeu0  29425  frgr3vlem2  30332  3vfriswmgrlem  30335  frgrncvvdeqlem2  30358  adjeu  31948  reuxfrdf  32548  rmoxfrd  32550  reueqi  36359  reueqbii  36360  cbvreuvw2  36399  cbvreudavw  36423  cbvreudavw2  36454  neibastop3  36532  cbvreud  37677  poimirlem25  37954  poimirlem27  37956  dfsuccl4  38783  fsuppind  43011  onsucf1olem  43686  pairreueq  47958  prprsprreu  47967  prprreueq  47968  reutru  49267