Definition df-reu 2460

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

This definition is referenced by:  nfreu1  2646  nfreudxy  2648  reubida  2656  reubiia  2659  reueq1f  2668  reu5  2687  rmo5  2690  cbvreu  2699  cbvreuvw  2707  reuv  2754  reu2  2923  reu6  2924  reu3  2925  2reuswapdc  2939  cbvreucsf  3119  reuss2  3413  reuun2  3416  reupick  3417  reupick3  3418  reusn  3660  rabsneu  3662  reuhypd  4465  funcnv3  5270  feu  5390  dff4im  5654  f1ompt  5659  fsn  5680  riotauni  5827  riotacl2  5834  riota1  5839  riota1a  5840  riota2df  5841  snriota  5850  riotaund  5855  acexmid  5864  climreu  11271  divalgb  11895  uptx  13325  txcn  13326  dedekindicc  13662  bdcriota  14175