Definition df-reu 2307

Description: Define restricted existential uniqueness. (Contributed by NM, 22-Nov-1994.)

Assertion

Ref	Expression
df-reu	⊢ (∃!x ∈ A φ ↔ ∃!x(x ∈ A ∧ φ))

Detailed syntax breakdown of Definition df-reu

Step	Hyp	Ref	Expression
1		wph	. . 3 wff φ
2		vx	. . 3 setvar x
3		cA	. . 3 class A
4	1, 2, 3	wreu 2302	. 2 wff ∃!x ∈ A φ
5	2	cv 1241	. . . . 5 class x
6	5, 3	wcel 1390	. . . 4 wff x ∈ A
7	6, 1	wa 97	. . 3 wff (x ∈ A ∧ φ)
8	7, 2	weu 1897	. 2 wff ∃!x(x ∈ A ∧ φ)
9	4, 8	wb 98	1 wff (∃!x ∈ A φ ↔ ∃!x(x ∈ A ∧ φ))

This definition is referenced by:  nfreu1  2475  nfreudxy  2477  reubida  2485  reubiia  2488  reueq1f  2497  reu5  2516  rmo5  2519  cbvreu  2525  reuv  2567  reu2  2723  reu6  2724  reu3  2725  2reuswapdc  2737  cbvreucsf  2904  reuss2  3211  reuun2  3214  reupick  3215  reupick3  3216  reusn  3432  rabsneu  3434  reuhypd  4169  funcnv3  4904  feu  5015  dff4im  5256  f1ompt  5263  fsn  5278  riotauni  5417  riotacl2  5424  riota1  5429  riota1a  5430  riota2df  5431  snriota  5440  riotaund  5445  acexmid  5454  bdcriota  9338