Definition df-reu 2535

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

This definition is referenced by:  nfreu1  2723  nfreudxy  2725  reubida  2734  reubiia  2738  reueq1f  2747  reu5  2770  rmo5  2773  cbvreu  2784  cbvreuvw  2792  reuv  2841  reu2  3014  reu6  3015  reu3  3016  2reuswapdc  3030  cbvreucsf  3212  reuss2  3513  reuun2  3516  reupick  3517  reupick3  3518  reusn  3778  rabsneu  3780  reuhypd  4612  funcnv3  5438  feu  5569  dff4im  5845  f1ompt  5850  fsn  5871  riotauni  6035  riotacl2  6043  riota1  6048  riota1a  6049  riota2df  6050  snriota  6060  riotaund  6065  acexmid  6074  climreu  12041  divalgb  12670  uptx  15298  txcn  15299  dedekindicc  15657  bdcriota  16823