Definition df-reu 2451

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

This definition is referenced by:  nfreu1  2637  nfreudxy  2639  reubida  2647  reubiia  2650  reueq1f  2659  reu5  2678  rmo5  2681  cbvreu  2690  cbvreuvw  2698  reuv  2745  reu2  2914  reu6  2915  reu3  2916  2reuswapdc  2930  cbvreucsf  3109  reuss2  3402  reuun2  3405  reupick  3406  reupick3  3407  reusn  3647  rabsneu  3649  reuhypd  4449  funcnv3  5250  feu  5370  dff4im  5631  f1ompt  5636  fsn  5657  riotauni  5804  riotacl2  5811  riota1  5816  riota1a  5817  riota2df  5818  snriota  5827  riotaund  5832  acexmid  5841  climreu  11238  divalgb  11862  uptx  12914  txcn  12915  dedekindicc  13251  bdcriota  13765