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  4619  funcnv3  5446  feu  5577  dff4im  5857  f1ompt  5862  fsn  5883  riotauni  6048  riotacl2  6056  riota1  6061  riota1a  6062  riota2df  6063  snriota  6073  riotaund  6078  acexmid  6087  climreu  12088  divalgb  12717  uptx  15500  txcn  15501  dedekindicc  15859  bdcriota  17114  dfralseu2  17371