Definition df-reu 3375

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 3060). (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 3372	. 2 wff ∃!𝑥 ∈ 𝐴 𝜑
5	2	cv 1538	. . . . 5 class 𝑥
6	5, 3	wcel 2104	. . . 4 wff 𝑥 ∈ 𝐴
7	6, 1	wa 394	. . 3 wff (𝑥 ∈ 𝐴 ∧ 𝜑)
8	7, 2	weu 2560	. 2 wff ∃!𝑥(𝑥 ∈ 𝐴 ∧ 𝜑)
9	4, 8	wb 205	1 wff (∃!𝑥 ∈ 𝐴 𝜑 ↔ ∃!𝑥(𝑥 ∈ 𝐴 ∧ 𝜑))

This definition is referenced by:  reu5  3376  reubiia  3381  reuanidOLD  3387  reubidva  3390  reueubd  3393  rmo5  3394  cbvreuvw  3398  reubida  3401  nfreu1  3406  nfreuw  3408  cbvreuwOLD  3410  reueq1OLD  3415  nfreuwOLD  3420  cbvreu  3422  nfreud  3427  reuv  3499  reurab  3696  reu2  3720  reu6  3721  reu3  3722  2reuswap  3741  2reuswap2  3742  2reu5lem1  3750  cbvreucsf  3939  reuun2  4313  reuss2  4314  reupick  4317  reupick3  4318  euelss  4320  reusn  4730  rabsneu  4732  reusv2lem4  5398  reusv2lem5  5399  reuhypd  5416  funcnv3  6617  feu  6766  dff4  7101  f1ompt  7111  fsn  7134  riotauni  7373  riotacl2  7384  riota1  7389  riota1a  7390  riota2df  7391  snriota  7401  riotaund  7407  aceq1  10114  dfac2b  10127  nqerf  10927  zmin  12932  climreu  15504  divalglem10  16349  divalgb  16351  uptx  23349  txcn  23350  q1peqb  25907  axcontlem2  28490  edgnbusgreu  28891  nbusgredgeu0  28892  frgr3vlem2  29794  3vfriswmgrlem  29797  frgrncvvdeqlem2  29820  adjeu  31409  reuxfrdf  31998  rmoxfrd  32000  neibastop3  35550  cbvreud  36557  poimirlem25  36816  poimirlem27  36818  fsuppind  41464  onsucf1olem  42322  pairreueq  46476  prprsprreu  46485  prprreueq  46486  reutru  47577