Definition df-reu 2462

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

This definition is referenced by:  nfreu1  2648  nfreudxy  2650  reubida  2658  reubiia  2661  reueq1f  2670  reu5  2689  rmo5  2692  cbvreu  2701  cbvreuvw  2709  reuv  2756  reu2  2925  reu6  2926  reu3  2927  2reuswapdc  2941  cbvreucsf  3121  reuss2  3415  reuun2  3418  reupick  3419  reupick3  3420  reusn  3663  rabsneu  3665  reuhypd  4471  funcnv3  5278  feu  5398  dff4im  5662  f1ompt  5667  fsn  5688  riotauni  5836  riotacl2  5843  riota1  5848  riota1a  5849  riota2df  5850  snriota  5859  riotaund  5864  acexmid  5873  climreu  11304  divalgb  11929  uptx  13744  txcn  13745  dedekindicc  14081  bdcriota  14605