Definition df-reu 2455

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 2450	. 2 wff ∃!𝑥 ∈ 𝐴 𝜑
5	2	cv 1347	. . . . 5 class 𝑥
6	5, 3	wcel 2141	. . . 4 wff 𝑥 ∈ 𝐴
7	6, 1	wa 103	. . 3 wff (𝑥 ∈ 𝐴 ∧ 𝜑)
8	7, 2	weu 2019	. 2 wff ∃!𝑥(𝑥 ∈ 𝐴 ∧ 𝜑)
9	4, 8	wb 104	1 wff (∃!𝑥 ∈ 𝐴 𝜑 ↔ ∃!𝑥(𝑥 ∈ 𝐴 ∧ 𝜑))

This definition is referenced by:  nfreu1  2641  nfreudxy  2643  reubida  2651  reubiia  2654  reueq1f  2663  reu5  2682  rmo5  2685  cbvreu  2694  cbvreuvw  2702  reuv  2749  reu2  2918  reu6  2919  reu3  2920  2reuswapdc  2934  cbvreucsf  3113  reuss2  3407  reuun2  3410  reupick  3411  reupick3  3412  reusn  3654  rabsneu  3656  reuhypd  4456  funcnv3  5260  feu  5380  dff4im  5642  f1ompt  5647  fsn  5668  riotauni  5815  riotacl2  5822  riota1  5827  riota1a  5828  riota2df  5829  snriota  5838  riotaund  5843  acexmid  5852  climreu  11260  divalgb  11884  uptx  13068  txcn  13069  dedekindicc  13405  bdcriota  13918