Definition df-reu 2479

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 2474	. 2 wff ∃!𝑥 ∈ 𝐴 𝜑
5	2	cv 1363	. . . . 5 class 𝑥
6	5, 3	wcel 2164	. . . 4 wff 𝑥 ∈ 𝐴
7	6, 1	wa 104	. . 3 wff (𝑥 ∈ 𝐴 ∧ 𝜑)
8	7, 2	weu 2042	. 2 wff ∃!𝑥(𝑥 ∈ 𝐴 ∧ 𝜑)
9	4, 8	wb 105	1 wff (∃!𝑥 ∈ 𝐴 𝜑 ↔ ∃!𝑥(𝑥 ∈ 𝐴 ∧ 𝜑))

This definition is referenced by:  nfreu1  2666  nfreudxy  2668  reubida  2676  reubiia  2679  reueq1f  2688  reu5  2711  rmo5  2714  cbvreu  2724  cbvreuvw  2732  reuv  2779  reu2  2948  reu6  2949  reu3  2950  2reuswapdc  2964  cbvreucsf  3145  reuss2  3439  reuun2  3442  reupick  3443  reupick3  3444  reusn  3689  rabsneu  3691  reuhypd  4502  funcnv3  5316  feu  5436  dff4im  5704  f1ompt  5709  fsn  5730  riotauni  5880  riotacl2  5887  riota1  5892  riota1a  5893  riota2df  5894  snriota  5903  riotaund  5908  acexmid  5917  climreu  11440  divalgb  12066  uptx  14442  txcn  14443  dedekindicc  14787  bdcriota  15375