Definition df-reu 3369

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

This definition is used by:  reu5  3370  reubiia  3375  reubidva  3382  reueubd  3385  rmo5  3386  cbvreuvw  3390  reubida  3392  nfreu1  3396  nfreuw  3398  reueqbidv  3404  cbvreu  3407  nfreud  3412  reuv  3482  reurab  3663  reu2  3687  reu6  3688  reu3  3689  2reuswap  3708  2reuswap2  3709  2reu5lem1  3717  cbvreucsf  3896  reuun2  4277  reuss2  4278  reupick  4281  reupick3  4282  euelss  4284  reusn  4692  rabsneu  4694  reusv2lem4  5371  reusv2lem5  5372  reuhypd  5389  funcnv3  6606  feu  6754  dff4  7096  f1ompt  7106  fsn  7131  riotauni  7375  riotacl2  7385  riota1  7390  riota1a  7391  riota2df  7392  snriota  7402  riotaund  7408  aceq1  10108  dfac2b  10121  nqerf  10921  zmin  12974  climreu  15614  divalglem10  16466  divalgb  16468  uptx  23793  txcn  23794  q1peqb  26324  axcontlem2  29326  edgnbusgreu  29728  nbusgredgeu0  29729  frgr3vlem2  30636  3vfriswmgrlem  30639  frgrncvvdeqlem2  30662  adjeu  32252  reuxfrdf  32848  rmoxfrd  32850  reueqi  36729  reueqbii  36730  cbvreuvw2  36769  cbvreudavw  36793  cbvreudavw2  36824  neibastop3  36901  cbvreud  38047  poimirlem25  38324  poimirlem27  38326  dfsuccl4  39151  fsuppind  43350  onsucf1olem  44025  pairreueq  48287  prprsprreu  48296  prprreueq  48297  reutru  49610  dfralseu2  50629