Definition df-reu 2517

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 2512	. 2 wff ∃!𝑥 ∈ 𝐴 𝜑
5	2	cv 1396	. . . . 5 class 𝑥
6	5, 3	wcel 2202	. . . 4 wff 𝑥 ∈ 𝐴
7	6, 1	wa 104	. . 3 wff (𝑥 ∈ 𝐴 ∧ 𝜑)
8	7, 2	weu 2079	. 2 wff ∃!𝑥(𝑥 ∈ 𝐴 ∧ 𝜑)
9	4, 8	wb 105	1 wff (∃!𝑥 ∈ 𝐴 𝜑 ↔ ∃!𝑥(𝑥 ∈ 𝐴 ∧ 𝜑))

This definition is referenced by:  nfreu1  2705  nfreudxy  2707  reubida  2715  reubiia  2719  reueq1f  2728  reu5  2751  rmo5  2754  cbvreu  2765  cbvreuvw  2773  reuv  2822  reu2  2994  reu6  2995  reu3  2996  2reuswapdc  3010  cbvreucsf  3192  reuss2  3487  reuun2  3490  reupick  3491  reupick3  3492  reusn  3742  rabsneu  3744  reuhypd  4568  funcnv3  5392  feu  5519  dff4im  5793  f1ompt  5798  fsn  5819  riotauni  5978  riotacl2  5986  riota1  5991  riota1a  5992  riota2df  5993  snriota  6003  riotaund  6008  acexmid  6017  climreu  11875  divalgb  12504  uptx  15017  txcn  15018  dedekindicc  15376  bdcriota  16529