Definition df-reu 3071

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 3069). (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 3066	. 2 wff ∃!𝑥 ∈ 𝐴 𝜑
5	2	cv 1542	. . . . 5 class 𝑥
6	5, 3	wcel 2112	. . . 4 wff 𝑥 ∈ 𝐴
7	6, 1	wa 399	. . 3 wff (𝑥 ∈ 𝐴 ∧ 𝜑)
8	7, 2	weu 2569	. 2 wff ∃!𝑥(𝑥 ∈ 𝐴 ∧ 𝜑)
9	4, 8	wb 209	1 wff (∃!𝑥 ∈ 𝐴 𝜑 ↔ ∃!𝑥(𝑥 ∈ 𝐴 ∧ 𝜑))

This definition is referenced by:  reuanid  3258  nfreu1  3297  nfreud  3299  nfreuw  3301  reubida  3314  reubidva  3315  reubiia  3317  reueq1f  3326  reueq1  3336  reu5  3352  rmo5  3356  reueubd  3358  cbvreuw  3366  cbvreu  3371  cbvreuvw  3376  reuv  3449  reu2  3656  reu6  3657  reu3  3658  2reuswap  3677  2reuswap2  3678  2reu5lem1  3686  cbvreucsf  3876  reuun2  4246  reuss2  4247  reupick  4250  reupick3  4251  euelss  4253  reusn  4660  rabsneu  4662  reusv2lem4  5318  reusv2lem5  5319  reuhypd  5336  funcnv3  6485  feu  6631  dff4  6956  f1ompt  6964  fsn  6986  riotauni  7215  riotacl2  7226  riota1  7231  riota1a  7232  riota2df  7233  snriota  7243  riotaund  7249  aceq1  9779  dfac2b  9792  nqerf  10592  zmin  12588  climreu  15168  divalglem10  16014  divalgb  16016  uptx  22659  txcn  22660  q1peqb  25199  axcontlem2  27211  edgnbusgreu  27612  nbusgredgeu0  27613  frgr3vlem2  28514  3vfriswmgrlem  28517  frgrncvvdeqlem2  28540  adjeu  30127  reuxfrdf  30715  rmoxfrd  30717  reurab  33551  neibastop3  34453  cbvreud  35450  poimirlem25  35708  poimirlem27  35710  fsuppind  40174  pairreueq  44823  prprsprreu  44832  prprreueq  44833  reutru  46012