Definition df-reu 2482

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

This definition is referenced by:  nfreu1  2669  nfreudxy  2671  reubida  2679  reubiia  2682  reueq1f  2691  reu5  2714  rmo5  2717  cbvreu  2727  cbvreuvw  2735  reuv  2782  reu2  2952  reu6  2953  reu3  2954  2reuswapdc  2968  cbvreucsf  3149  reuss2  3444  reuun2  3447  reupick  3448  reupick3  3449  reusn  3694  rabsneu  3696  reuhypd  4507  funcnv3  5321  feu  5443  dff4im  5711  f1ompt  5716  fsn  5737  riotauni  5887  riotacl2  5894  riota1  5899  riota1a  5900  riota2df  5901  snriota  5910  riotaund  5915  acexmid  5924  climreu  11479  divalgb  12107  uptx  14594  txcn  14595  dedekindicc  14953  bdcriota  15613