Definition df-reu 2515

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

This definition is referenced by:  nfreu1  2703  nfreudxy  2705  reubida  2713  reubiia  2717  reueq1f  2726  reu5  2749  rmo5  2752  cbvreu  2763  cbvreuvw  2771  reuv  2819  reu2  2991  reu6  2992  reu3  2993  2reuswapdc  3007  cbvreucsf  3189  reuss2  3484  reuun2  3487  reupick  3488  reupick3  3489  reusn  3737  rabsneu  3739  reuhypd  4562  funcnv3  5383  feu  5510  dff4im  5783  f1ompt  5788  fsn  5809  riotauni  5967  riotacl2  5975  riota1  5980  riota1a  5981  riota2df  5982  snriota  5992  riotaund  5997  acexmid  6006  climreu  11816  divalgb  12444  uptx  14956  txcn  14957  dedekindicc  15315  bdcriota  16270