Definition df-reu 2492

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

This definition is referenced by:  nfreu1  2679  nfreudxy  2681  reubida  2689  reubiia  2692  reueq1f  2701  reu5  2724  rmo5  2727  cbvreu  2737  cbvreuvw  2745  reuv  2792  reu2  2962  reu6  2963  reu3  2964  2reuswapdc  2978  cbvreucsf  3159  reuss2  3454  reuun2  3457  reupick  3458  reupick3  3459  reusn  3705  rabsneu  3707  reuhypd  4522  funcnv3  5341  feu  5465  dff4im  5733  f1ompt  5738  fsn  5759  riotauni  5913  riotacl2  5920  riota1  5925  riota1a  5926  riota2df  5927  snriota  5936  riotaund  5941  acexmid  5950  climreu  11652  divalgb  12280  uptx  14790  txcn  14791  dedekindicc  15149  bdcriota  15893