Definition df-reu 2313

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 2308	. 2 wff ∃!𝑥 ∈ 𝐴 𝜑
5	2	cv 1242	. . . . 5 class 𝑥
6	5, 3	wcel 1393	. . . 4 wff 𝑥 ∈ 𝐴
7	6, 1	wa 97	. . 3 wff (𝑥 ∈ 𝐴 ∧ 𝜑)
8	7, 2	weu 1900	. 2 wff ∃!𝑥(𝑥 ∈ 𝐴 ∧ 𝜑)
9	4, 8	wb 98	1 wff (∃!𝑥 ∈ 𝐴 𝜑 ↔ ∃!𝑥(𝑥 ∈ 𝐴 ∧ 𝜑))

This definition is referenced by:  nfreu1  2481  nfreudxy  2483  reubida  2491  reubiia  2494  reueq1f  2503  reu5  2522  rmo5  2525  cbvreu  2531  reuv  2573  reu2  2729  reu6  2730  reu3  2731  2reuswapdc  2743  cbvreucsf  2910  reuss2  3217  reuun2  3220  reupick  3221  reupick3  3222  reusn  3441  rabsneu  3443  reuhypd  4203  funcnv3  4961  feu  5072  dff4im  5313  f1ompt  5320  fsn  5335  riotauni  5474  riotacl2  5481  riota1  5486  riota1a  5487  riota2df  5488  snriota  5497  riotaund  5502  acexmid  5511  climreu  9818  bdcriota  10003