Definition df-reu 3389

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

This definition is referenced by:  reu5  3390  reubiia  3395  reuanidOLD  3401  reubidva  3404  reueubd  3407  rmo5  3408  cbvreuvw  3412  reubida  3415  nfreu1  3420  nfreuw  3422  cbvreuwOLD  3423  reueq1OLD  3428  nfreuwOLD  3433  cbvreu  3435  nfreud  3440  reuv  3518  reurab  3723  reu2  3747  reu6  3748  reu3  3749  2reuswap  3768  2reuswap2  3769  2reu5lem1  3777  cbvreucsf  3968  reuun2  4344  reuss2  4345  reupick  4348  reupick3  4349  euelss  4351  reusn  4752  rabsneu  4754  reusv2lem4  5419  reusv2lem5  5420  reuhypd  5437  funcnv3  6648  feu  6797  dff4  7135  f1ompt  7145  fsn  7169  riotauni  7410  riotacl2  7421  riota1  7426  riota1a  7427  riota2df  7428  snriota  7438  riotaund  7444  aceq1  10186  dfac2b  10200  nqerf  10999  zmin  13009  climreu  15602  divalglem10  16450  divalgb  16452  uptx  23654  txcn  23655  q1peqb  26215  axcontlem2  28998  edgnbusgreu  29402  nbusgredgeu0  29403  frgr3vlem2  30306  3vfriswmgrlem  30309  frgrncvvdeqlem2  30332  adjeu  31921  reuxfrdf  32519  rmoxfrd  32521  reueqi  36153  reueqbii  36154  reueqbidv  36179  cbvreuvw2  36195  cbvreudavw  36219  cbvreudavw2  36250  neibastop3  36328  cbvreud  37339  poimirlem25  37605  poimirlem27  37607  fsuppind  42545  onsucf1olem  43232  pairreueq  47384  prprsprreu  47393  prprreueq  47394  reutru  48537