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 used 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  3782  rabsneu  3784  reuhypd  4617  funcnv3  5443  feu  5574  dff4im  5854  f1ompt  5859  fsn  5880  riotauni  6045  riotacl2  6053  riota1  6058  riota1a  6059  riota2df  6060  snriota  6070  riotaund  6075  acexmid  6084  climreu  12063  divalgb  12692  uptx  15375  txcn  15376  dedekindicc  15734  bdcriota  16909  dfralseu2  17164