Definition df-reu 2423

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

This definition is referenced by:  nfreu1  2602  nfreudxy  2604  reubida  2612  reubiia  2615  reueq1f  2624  reu5  2643  rmo5  2646  cbvreu  2652  reuv  2705  reu2  2872  reu6  2873  reu3  2874  2reuswapdc  2888  cbvreucsf  3064  reuss2  3356  reuun2  3359  reupick  3360  reupick3  3361  reusn  3594  rabsneu  3596  reuhypd  4392  funcnv3  5185  feu  5305  dff4im  5566  f1ompt  5571  fsn  5592  riotauni  5736  riotacl2  5743  riota1  5748  riota1a  5749  riota2df  5750  snriota  5759  riotaund  5764  acexmid  5773  climreu  11066  divalgb  11622  uptx  12443  txcn  12444  dedekindicc  12780  bdcriota  13081