Definition df-reu 2529

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

This definition is referenced by:  nfreu1  2717  nfreudxy  2719  reubida  2728  reubiia  2732  reueq1f  2741  reu5  2764  rmo5  2767  cbvreu  2778  cbvreuvw  2786  reuv  2835  reu2  3008  reu6  3009  reu3  3010  2reuswapdc  3024  cbvreucsf  3206  reuss2  3505  reuun2  3508  reupick  3509  reupick3  3510  reusn  3767  rabsneu  3769  reuhypd  4597  funcnv3  5423  feu  5554  dff4im  5828  f1ompt  5833  fsn  5854  riotauni  6018  riotacl2  6026  riota1  6031  riota1a  6032  riota2df  6033  snriota  6043  riotaund  6048  acexmid  6057  climreu  12007  divalgb  12636  uptx  15265  txcn  15266  dedekindicc  15624  bdcriota  16779