Definition df-reu 2362

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 2357	. 2 wff ∃!𝑥 ∈ 𝐴 𝜑
5	2	cv 1286	. . . . 5 class 𝑥
6	5, 3	wcel 1436	. . . 4 wff 𝑥 ∈ 𝐴
7	6, 1	wa 102	. . 3 wff (𝑥 ∈ 𝐴 ∧ 𝜑)
8	7, 2	weu 1945	. 2 wff ∃!𝑥(𝑥 ∈ 𝐴 ∧ 𝜑)
9	4, 8	wb 103	1 wff (∃!𝑥 ∈ 𝐴 𝜑 ↔ ∃!𝑥(𝑥 ∈ 𝐴 ∧ 𝜑))

This definition is referenced by:  nfreu1  2534  nfreudxy  2536  reubida  2544  reubiia  2547  reueq1f  2556  reu5  2575  rmo5  2578  cbvreu  2584  reuv  2632  reu2  2794  reu6  2795  reu3  2796  2reuswapdc  2808  cbvreucsf  2981  reuss2  3268  reuun2  3271  reupick  3272  reupick3  3273  reusn  3498  rabsneu  3500  reuhypd  4269  funcnv3  5043  feu  5158  dff4im  5410  f1ompt  5415  fsn  5434  riotauni  5577  riotacl2  5584  riota1  5589  riota1a  5590  riota2df  5591  snriota  5600  riotaund  5605  acexmid  5614  climreu  10583  divalgb  10831  bdcriota  11243