Definition df-reu 2287

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 2282	. 2 wff ∃!x ∈ A φ
5	2	cv 1225	. . . . 5 class x
6	5, 3	wcel 1370	. . . 4 wff x ∈ A
7	6, 1	wa 97	. . 3 wff (x ∈ A ∧ φ)
8	7, 2	weu 1878	. 2 wff ∃!x(x ∈ A ∧ φ)
9	4, 8	wb 98	1 wff (∃!x ∈ A φ ↔ ∃!x(x ∈ A ∧ φ))

This definition is referenced by:  nfreu1  2455  nfreudxy  2457  reubida  2465  reubiia  2468  reueq1f  2477  reu5  2496  rmo5  2499  cbvreu  2505  reuv  2546  reu2  2702  reu6  2703  reu3  2704  2reuswapdc  2716  cbvreucsf  2883  reuss2  3190  reuun2  3193  reupick  3194  reupick3  3195  reusn  3411  rabsneu  3413  reuhypd  4149  funcnv3  4883  feu  4993  dff4im  5234  f1ompt  5241  fsn  5256  riotauni  5394  riotacl2  5401  riota1  5406  riota1a  5407  riota2df  5408  snriota  5417  riotaund  5422  acexmid  5431  bdcriota  7249