Definition df-reu 2282

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

This definition is referenced by:  nfreu1  2450  nfreudxy  2452  reubida  2460  reubiia  2463  reueq1f  2472  reu5  2491  rmo5  2494  cbvreu  2500  reuv  2541  reu2  2697  reu6  2698  reu3  2699  2reuswapdc  2711  cbvreucsf  2878  reuss2  3185  reuun2  3188  reupick  3189  reupick3  3190  reusn  3404  rabsneu  3406  reuhypd  4141  funcnv3  4875  feu  4985  dff4im  5226  f1ompt  5233  fsn  5248  riotauni  5386  riotacl2  5393  riota1  5398  riota1a  5399  riota2df  5400  snriota  5409  riotaund  5414  acexmid  5423  bdcriota  8268