Definition df-reu 2462

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

This definition is referenced by:  nfreu1  2649  nfreudxy  2651  reubida  2659  reubiia  2662  reueq1f  2671  reu5  2690  rmo5  2693  cbvreu  2702  cbvreuvw  2710  reuv  2757  reu2  2926  reu6  2927  reu3  2928  2reuswapdc  2942  cbvreucsf  3122  reuss2  3416  reuun2  3419  reupick  3420  reupick3  3421  reusn  3664  rabsneu  3666  reuhypd  4472  funcnv3  5279  feu  5399  dff4im  5663  f1ompt  5668  fsn  5689  riotauni  5837  riotacl2  5844  riota1  5849  riota1a  5850  riota2df  5851  snriota  5860  riotaund  5865  acexmid  5874  climreu  11305  divalgb  11930  uptx  13777  txcn  13778  dedekindicc  14114  bdcriota  14638