Definition df-reu 2517

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

This definition is referenced by:  nfreu1  2705  nfreudxy  2707  reubida  2715  reubiia  2719  reueq1f  2728  reu5  2751  rmo5  2754  cbvreu  2765  cbvreuvw  2773  reuv  2822  reu2  2994  reu6  2995  reu3  2996  2reuswapdc  3010  cbvreucsf  3192  reuss2  3487  reuun2  3490  reupick  3491  reupick3  3492  reusn  3742  rabsneu  3744  reuhypd  4568  funcnv3  5392  feu  5519  dff4im  5793  f1ompt  5798  fsn  5819  riotauni  5977  riotacl2  5985  riota1  5990  riota1a  5991  riota2df  5992  snriota  6002  riotaund  6007  acexmid  6016  climreu  11857  divalgb  12485  uptx  14997  txcn  14998  dedekindicc  15356  bdcriota  16478