Definition df-reu 3368

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 3079). (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 3365	. 2 wff ∃!𝑥 ∈ 𝐴 𝜑
5	2	cv 1569	. . . . 5 class 𝑥
6	5, 3	wcel 2145	. . . 4 wff 𝑥 ∈ 𝐴
7	6, 1	wa 401	. . 3 wff (𝑥 ∈ 𝐴 ∧ 𝜑)
8	7, 2	weu 2595	. 2 wff ∃!𝑥(𝑥 ∈ 𝐴 ∧ 𝜑)
9	4, 8	wb 209	1 wff (∃!𝑥 ∈ 𝐴 𝜑 ↔ ∃!𝑥(𝑥 ∈ 𝐴 ∧ 𝜑))

This definition is used by:  reu5  3369  reubiia  3374  reubidva  3381  reueubd  3384  rmo5  3385  cbvreuvw  3389  reubida  3391  nfreu1  3395  nfreuw  3397  reueqbidv  3403  cbvreu  3406  nfreud  3411  reuv  3481  reurab  3662  reu2  3686  reu6  3687  reu3  3688  2reuswap  3707  2reuswap2  3708  2reu5lem1  3716  cbvreucsf  3894  reuun2  4274  reuss2  4275  reupick  4278  reupick3  4279  euelss  4281  reusn  4691  rabsneu  4693  reusv2lem4  5370  reusv2lem5  5371  reuhypd  5388  funcnv3  6607  feu  6755  dff4  7097  f1ompt  7107  fsn  7132  riotauni  7379  riotacl2  7389  riota1  7394  riota1a  7395  riota2df  7396  snriota  7406  riotaund  7412  aceq1  10123  dfac2b  10136  nqerf  10942  zmin  12996  climreu  15645  divalglem10  16496  divalgb  16498  uptx  23852  txcn  23853  q1peqb  26383  axcontlem2  29408  edgnbusgreu  29813  nbusgredgeu0  29814  frgr3vlem2  30740  3vfriswmgrlem  30743  frgrncvvdeqlem2  30766  adjeu  32356  reuxfrdf  32952  rmoxfrd  32954  reueqi  36796  reueqbii  36797  cbvreuvw2  36836  cbvreudavw  36860  cbvreudavw2  36891  neibastop3  36968  cbvreud  38114  poimirlem25  38381  poimirlem27  38383  dfsuccl4  39209  fsuppind  43423  onsucf1olem  44098  pairreueq  48397  prprsprreu  48406  prprreueq  48407  reutru  49719  dfralseu2  50739