Definition df-reu 2518

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 2513	. 2 wff ∃!𝑥 ∈ 𝐴 𝜑
5	2	cv 1397	. . . . 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  2706  nfreudxy  2708  reubida  2716  reubiia  2720  reueq1f  2729  reu5  2752  rmo5  2755  cbvreu  2766  cbvreuvw  2774  reuv  2823  reu2  2995  reu6  2996  reu3  2997  2reuswapdc  3011  cbvreucsf  3193  reuss2  3489  reuun2  3492  reupick  3493  reupick3  3494  reusn  3746  rabsneu  3748  reuhypd  4574  funcnv3  5399  feu  5527  dff4im  5801  f1ompt  5806  fsn  5827  riotauni  5988  riotacl2  5996  riota1  6001  riota1a  6002  riota2df  6003  snriota  6013  riotaund  6018  acexmid  6027  climreu  11937  divalgb  12566  uptx  15085  txcn  15086  dedekindicc  15444  bdcriota  16599