Definition df-reu 2495

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

This definition is referenced by:  nfreu1  2683  nfreudxy  2685  reubida  2693  reubiia  2697  reueq1f  2706  reu5  2729  rmo5  2732  cbvreu  2743  cbvreuvw  2751  reuv  2799  reu2  2971  reu6  2972  reu3  2973  2reuswapdc  2987  cbvreucsf  3169  reuss2  3464  reuun2  3467  reupick  3468  reupick3  3469  reusn  3717  rabsneu  3719  reuhypd  4539  funcnv3  5359  feu  5484  dff4im  5754  f1ompt  5759  fsn  5780  riotauni  5934  riotacl2  5942  riota1  5947  riota1a  5948  riota2df  5949  snriota  5959  riotaund  5964  acexmid  5973  climreu  11774  divalgb  12402  uptx  14913  txcn  14914  dedekindicc  15272  bdcriota  16156