Definition df-reu 3073

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 3071). (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 3068	. 2 wff ∃!𝑥 ∈ 𝐴 𝜑
5	2	cv 1541	. . . . 5 class 𝑥
6	5, 3	wcel 2110	. . . 4 wff 𝑥 ∈ 𝐴
7	6, 1	wa 396	. . 3 wff (𝑥 ∈ 𝐴 ∧ 𝜑)
8	7, 2	weu 2570	. 2 wff ∃!𝑥(𝑥 ∈ 𝐴 ∧ 𝜑)
9	4, 8	wb 205	1 wff (∃!𝑥 ∈ 𝐴 𝜑 ↔ ∃!𝑥(𝑥 ∈ 𝐴 ∧ 𝜑))

This definition is referenced by:  reuanid  3259  nfreu1  3299  nfreud  3301  nfreuw  3304  nfreuwOLD  3305  reubida  3320  reubidva  3321  reubiia  3323  reueq1f  3333  reueq1  3343  reu5  3360  rmo5  3364  reueubd  3366  cbvreuw  3374  cbvreu  3379  cbvreuvw  3384  reuv  3457  reu2  3664  reu6  3665  reu3  3666  2reuswap  3685  2reuswap2  3686  2reu5lem1  3694  cbvreucsf  3884  reuun2  4254  reuss2  4255  reupick  4258  reupick3  4259  euelss  4261  reusn  4669  rabsneu  4671  reusv2lem4  5328  reusv2lem5  5329  reuhypd  5346  funcnv3  6501  feu  6647  dff4  6972  f1ompt  6980  fsn  7002  riotauni  7232  riotacl2  7243  riota1  7248  riota1a  7249  riota2df  7250  snriota  7260  riotaund  7266  aceq1  9872  dfac2b  9885  nqerf  10685  zmin  12681  climreu  15261  divalglem10  16107  divalgb  16109  uptx  22772  txcn  22773  q1peqb  25315  axcontlem2  27329  edgnbusgreu  27730  nbusgredgeu0  27731  frgr3vlem2  28632  3vfriswmgrlem  28635  frgrncvvdeqlem2  28658  adjeu  30245  reuxfrdf  30833  rmoxfrd  30835  reurab  33668  neibastop3  34545  cbvreud  35538  poimirlem25  35796  poimirlem27  35798  fsuppind  40274  pairreueq  44929  prprsprreu  44938  prprreueq  44939  reutru  46118