Definition df-reu 3088

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 3086). (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 3083	. 2 wff ∃!𝑥 ∈ 𝐴 𝜑
5	2	cv 1507	. . . . 5 class 𝑥
6	5, 3	wcel 2051	. . . 4 wff 𝑥 ∈ 𝐴
7	6, 1	wa 387	. . 3 wff (𝑥 ∈ 𝐴 ∧ 𝜑)
8	7, 2	weu 2584	. 2 wff ∃!𝑥(𝑥 ∈ 𝐴 ∧ 𝜑)
9	4, 8	wb 198	1 wff (∃!𝑥 ∈ 𝐴 𝜑 ↔ ∃!𝑥(𝑥 ∈ 𝐴 ∧ 𝜑))

This definition is referenced by:  reuanid  3262  nfreu1  3304  nfreud  3306  reubida  3319  reubidva  3320  reubiia  3323  reueq1f  3332  reueq1  3340  reu5  3363  rmo5  3367  reueubd  3369  cbvreu  3374  reuv  3435  reu2  3621  reu6  3622  reu3  3623  2reuswap  3642  2reuswap2  3643  2reu5lem1  3648  cbvreucsf  3815  reuss2  4164  reuun2  4167  reupick  4168  reupick3  4169  euelss  4171  reusn  4533  rabsneu  4535  reusv2lem4  5151  reusv2lem5  5152  reuhypd  5172  funcnv3  6254  feu  6380  dff4  6688  f1ompt  6696  fsn  6718  riotauni  6941  riotacl2  6948  riota1  6953  riota1a  6954  riota2df  6955  snriota  6965  riotaund  6971  aceq1  9335  dfac2b  9348  nqerf  10148  zmin  12156  climreu  14772  divalglem10  15611  divalgb  15613  uptx  21952  txcn  21953  q1peqb  24466  axcontlem2  26469  edgnbusgreu  26867  nbusgredgeu0  26868  frgr3vlem2  27823  3vfriswmgrlem  27826  frgrncvvdeqlem2  27849  adjeu  29462  rmoxfrd  30053  neibastop3  33268  cbvreud  34133  poimirlem25  34395  poimirlem27  34397  pairreueq  43072  prprsprreu  43081  prprreueq  43082