Definition df-reu 3360

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 3052). (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 3357	. 2 wff ∃!𝑥 ∈ 𝐴 𝜑
5	2	cv 1539	. . . . 5 class 𝑥
6	5, 3	wcel 2108	. . . 4 wff 𝑥 ∈ 𝐴
7	6, 1	wa 395	. . 3 wff (𝑥 ∈ 𝐴 ∧ 𝜑)
8	7, 2	weu 2567	. 2 wff ∃!𝑥(𝑥 ∈ 𝐴 ∧ 𝜑)
9	4, 8	wb 206	1 wff (∃!𝑥 ∈ 𝐴 𝜑 ↔ ∃!𝑥(𝑥 ∈ 𝐴 ∧ 𝜑))

This definition is referenced by:  reu5  3361  reubiia  3366  reuanidOLD  3372  reubidva  3375  reueubd  3378  rmo5  3379  cbvreuvw  3383  reubida  3386  nfreu1  3391  nfreuw  3393  cbvreuwOLD  3394  reueq1OLD  3398  reueqbidv  3402  nfreuwOLD  3405  cbvreu  3407  nfreud  3412  reuv  3489  reurab  3684  reu2  3708  reu6  3709  reu3  3710  2reuswap  3729  2reuswap2  3730  2reu5lem1  3738  cbvreucsf  3918  reuun2  4300  reuss2  4301  reupick  4304  reupick3  4305  euelss  4307  reusn  4703  rabsneu  4705  reusv2lem4  5371  reusv2lem5  5372  reuhypd  5389  funcnv3  6605  feu  6753  dff4  7090  f1ompt  7100  fsn  7124  riotauni  7366  riotacl2  7376  riota1  7381  riota1a  7382  riota2df  7383  snriota  7393  riotaund  7399  aceq1  10129  dfac2b  10143  nqerf  10942  zmin  12958  climreu  15570  divalglem10  16419  divalgb  16421  uptx  23561  txcn  23562  q1peqb  26111  axcontlem2  28890  edgnbusgreu  29292  nbusgredgeu0  29293  frgr3vlem2  30201  3vfriswmgrlem  30204  frgrncvvdeqlem2  30227  adjeu  31816  reuxfrdf  32418  rmoxfrd  32420  reueqi  36153  reueqbii  36154  cbvreuvw2  36193  cbvreudavw  36217  cbvreudavw2  36248  neibastop3  36326  cbvreud  37337  poimirlem25  37615  poimirlem27  37617  fsuppind  42560  onsucf1olem  43241  pairreueq  47472  prprsprreu  47481  prprreueq  47482  reutru  48731