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  2820  reu2  2992  reu6  2993  reu3  2994  2reuswapdc  3008  cbvreucsf  3190  reuss2  3485  reuun2  3488  reupick  3489  reupick3  3490  reusn  3738  rabsneu  3740  reuhypd  4564  funcnv3  5387  feu  5514  dff4im  5787  f1ompt  5792  fsn  5813  riotauni  5971  riotacl2  5979  riota1  5984  riota1a  5985  riota2df  5986  snriota  5996  riotaund  6001  acexmid  6010  climreu  11845  divalgb  12473  uptx  14985  txcn  14986  dedekindicc  15344  bdcriota  16388