Definition df-reu 2527

Description: Define restricted existential uniqueness. (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 2522	. 2 wff ∃!𝑥 ∈ 𝐴 𝜑
5	2	cv 1397	. . . . 5 class 𝑥
6	5, 3	wcel 2203	. . . 4 wff 𝑥 ∈ 𝐴
7	6, 1	wa 104	. . 3 wff (𝑥 ∈ 𝐴 ∧ 𝜑)
8	7, 2	weu 2080	. 2 wff ∃!𝑥(𝑥 ∈ 𝐴 ∧ 𝜑)
9	4, 8	wb 105	1 wff (∃!𝑥 ∈ 𝐴 𝜑 ↔ ∃!𝑥(𝑥 ∈ 𝐴 ∧ 𝜑))

This definition is referenced by:  nfreu1  2715  nfreudxy  2717  reubida  2726  reubiia  2730  reueq1f  2739  reu5  2762  rmo5  2765  cbvreu  2776  cbvreuvw  2784  reuv  2833  reu2  3005  reu6  3006  reu3  3007  2reuswapdc  3021  cbvreucsf  3203  reuss2  3501  reuun2  3504  reupick  3505  reupick3  3506  reusn  3762  rabsneu  3764  reuhypd  4592  funcnv3  5418  feu  5549  dff4im  5823  f1ompt  5828  fsn  5849  riotauni  6010  riotacl2  6018  riota1  6023  riota1a  6024  riota2df  6025  snriota  6035  riotaund  6040  acexmid  6049  climreu  11982  divalgb  12611  uptx  15139  txcn  15140  dedekindicc  15498  bdcriota  16653