Definition df-reu 3344

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 3341	. 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  3345  reubiia  3350  reubidva  3357  reueubd  3360  rmo5  3361  cbvreuvw  3365  reubida  3367  nfreu1  3371  nfreuw  3373  reueqbidv  3379  cbvreu  3382  nfreud  3387  reuv  3459  reurab  3648  reu2  3672  reu6  3673  reu3  3674  2reuswap  3693  2reuswap2  3694  2reu5lem1  3702  cbvreucsf  3882  reuun2  4266  reuss2  4267  reupick  4270  reupick3  4271  euelss  4273  reusn  4672  rabsneu  4674  reusv2lem4  5342  reusv2lem5  5343  reuhypd  5360  funcnv3  6566  feu  6714  dff4  7051  f1ompt  7061  fsn  7086  riotauni  7327  riotacl2  7337  riota1  7342  riota1a  7343  riota2df  7344  snriota  7354  riotaund  7360  aceq1  10036  dfac2b  10050  nqerf  10850  zmin  12891  climreu  15515  divalglem10  16368  divalgb  16370  uptx  23587  txcn  23588  q1peqb  26118  axcontlem2  29031  edgnbusgreu  29433  nbusgredgeu0  29434  frgr3vlem2  30341  3vfriswmgrlem  30344  frgrncvvdeqlem2  30367  adjeu  31957  reuxfrdf  32557  rmoxfrd  32559  reueqi  36368  reueqbii  36369  cbvreuvw2  36408  cbvreudavw  36432  cbvreudavw2  36463  neibastop3  36541  cbvreud  37686  poimirlem25  37963  poimirlem27  37965  dfsuccl4  38792  fsuppind  43020  onsucf1olem  43695  pairreueq  47961  prprsprreu  47970  prprreueq  47971  reutru  49270