Definition df-reu 3347

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 3048). (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 3344	. 2 wff ∃!𝑥 ∈ 𝐴 𝜑
5	2	cv 1540	. . . . 5 class 𝑥
6	5, 3	wcel 2111	. . . 4 wff 𝑥 ∈ 𝐴
7	6, 1	wa 395	. . 3 wff (𝑥 ∈ 𝐴 ∧ 𝜑)
8	7, 2	weu 2563	. 2 wff ∃!𝑥(𝑥 ∈ 𝐴 ∧ 𝜑)
9	4, 8	wb 206	1 wff (∃!𝑥 ∈ 𝐴 𝜑 ↔ ∃!𝑥(𝑥 ∈ 𝐴 ∧ 𝜑))

This definition is referenced by:  reu5  3348  reubiia  3353  reubidva  3360  reueubd  3363  rmo5  3364  cbvreuvw  3368  reubida  3370  nfreu1  3374  nfreuw  3376  reueq1OLD  3380  reueqbidv  3384  cbvreu  3387  nfreud  3392  reuv  3465  reurab  3655  reu2  3679  reu6  3680  reu3  3681  2reuswap  3700  2reuswap2  3701  2reu5lem1  3709  cbvreucsf  3889  reuun2  4274  reuss2  4275  reupick  4278  reupick3  4279  euelss  4281  reusn  4679  rabsneu  4681  reusv2lem4  5341  reusv2lem5  5342  reuhypd  5359  funcnv3  6557  feu  6705  dff4  7040  f1ompt  7050  fsn  7074  riotauni  7315  riotacl2  7325  riota1  7330  riota1a  7331  riota2df  7332  snriota  7342  riotaund  7348  aceq1  10014  dfac2b  10028  nqerf  10827  zmin  12848  climreu  15469  divalglem10  16319  divalgb  16321  uptx  23546  txcn  23547  q1peqb  26094  axcontlem2  28950  edgnbusgreu  29352  nbusgredgeu0  29353  frgr3vlem2  30261  3vfriswmgrlem  30264  frgrncvvdeqlem2  30287  adjeu  31876  reuxfrdf  32477  rmoxfrd  32479  reueqi  36240  reueqbii  36241  cbvreuvw2  36280  cbvreudavw  36304  cbvreudavw2  36335  neibastop3  36413  cbvreud  37424  poimirlem25  37691  poimirlem27  37693  dfsuccl4  38493  fsuppind  42689  onsucf1olem  43368  pairreueq  47615  prprsprreu  47624  prprreueq  47625  reutru  48909