Definition df-reu 3352

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 3061). (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 3349	. 2 wff ∃!𝑥 ∈ 𝐴 𝜑
5	2	cv 1540	. . . . 5 class 𝑥
6	5, 3	wcel 2106	. . . 4 wff 𝑥 ∈ 𝐴
7	6, 1	wa 396	. . 3 wff (𝑥 ∈ 𝐴 ∧ 𝜑)
8	7, 2	weu 2561	. 2 wff ∃!𝑥(𝑥 ∈ 𝐴 ∧ 𝜑)
9	4, 8	wb 205	1 wff (∃!𝑥 ∈ 𝐴 𝜑 ↔ ∃!𝑥(𝑥 ∈ 𝐴 ∧ 𝜑))

This definition is referenced by:  reu5  3353  reubiia  3358  reuanidOLD  3364  reubidva  3367  reueubd  3370  rmo5  3371  cbvreuvw  3375  reubida  3378  nfreu1  3383  nfreuw  3385  cbvreuwOLD  3387  reueq1  3390  reueq1f  3394  nfreuwOLD  3395  cbvreu  3397  nfreud  3402  reuv  3472  reurab  3662  reu2  3686  reu6  3687  reu3  3688  2reuswap  3707  2reuswap2  3708  2reu5lem1  3716  cbvreucsf  3905  reuun2  4279  reuss2  4280  reupick  4283  reupick3  4284  euelss  4286  reusn  4693  rabsneu  4695  reusv2lem4  5361  reusv2lem5  5362  reuhypd  5379  funcnv3  6576  feu  6723  dff4  7056  f1ompt  7064  fsn  7086  riotauni  7324  riotacl2  7335  riota1  7340  riota1a  7341  riota2df  7342  snriota  7352  riotaund  7358  aceq1  10062  dfac2b  10075  nqerf  10875  zmin  12878  climreu  15450  divalglem10  16295  divalgb  16297  uptx  23013  txcn  23014  q1peqb  25556  axcontlem2  27977  edgnbusgreu  28378  nbusgredgeu0  28379  frgr3vlem2  29281  3vfriswmgrlem  29284  frgrncvvdeqlem2  29307  adjeu  30894  reuxfrdf  31483  rmoxfrd  31485  neibastop3  34910  cbvreud  35917  poimirlem25  36176  poimirlem27  36178  fsuppind  40823  onsucf1olem  41663  pairreueq  45822  prprsprreu  45831  prprreueq  45832  reutru  47010