Definition df-reu 3113

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 3111). (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 3108	. 2 wff ∃!𝑥 ∈ 𝐴 𝜑
5	2	cv 1537	. . . . 5 class 𝑥
6	5, 3	wcel 2111	. . . 4 wff 𝑥 ∈ 𝐴
7	6, 1	wa 399	. . 3 wff (𝑥 ∈ 𝐴 ∧ 𝜑)
8	7, 2	weu 2628	. 2 wff ∃!𝑥(𝑥 ∈ 𝐴 ∧ 𝜑)
9	4, 8	wb 209	1 wff (∃!𝑥 ∈ 𝐴 𝜑 ↔ ∃!𝑥(𝑥 ∈ 𝐴 ∧ 𝜑))

This definition is referenced by:  reuanid  3286  nfreu1  3323  nfreud  3325  nfreuw  3327  reubida  3340  reubidva  3341  reubiia  3343  reueq1f  3352  reueq1  3360  reu5  3375  rmo5  3379  reueubd  3381  cbvreuw  3389  cbvreu  3394  reuv  3468  reu2  3664  reu6  3665  reu3  3666  2reuswap  3685  2reuswap2  3686  2reu5lem1  3694  cbvreucsf  3872  reuss2  4235  reuun2  4238  reupick  4239  reupick3  4240  euelss  4242  reusn  4623  rabsneu  4625  reusv2lem4  5267  reusv2lem5  5268  reuhypd  5285  funcnv3  6394  feu  6528  dff4  6844  f1ompt  6852  fsn  6874  riotauni  7099  riotacl2  7109  riota1  7114  riota1a  7115  riota2df  7116  snriota  7126  riotaund  7132  aceq1  9528  dfac2b  9541  nqerf  10341  zmin  12332  climreu  14905  divalglem10  15743  divalgb  15745  uptx  22230  txcn  22231  q1peqb  24755  axcontlem2  26759  edgnbusgreu  27157  nbusgredgeu0  27158  frgr3vlem2  28059  3vfriswmgrlem  28062  frgrncvvdeqlem2  28085  adjeu  29672  reuxfrdf  30262  rmoxfrd  30264  neibastop3  33823  cbvreud  34790  poimirlem25  35082  poimirlem27  35084  fsuppind  39456  pairreueq  44027  prprsprreu  44036  prprreueq  44037