Definition df-reu 2382

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

This definition is referenced by:  nfreu1  2560  nfreudxy  2562  reubida  2570  reubiia  2573  reueq1f  2582  reu5  2601  rmo5  2604  cbvreu  2610  reuv  2660  reu2  2825  reu6  2826  reu3  2827  2reuswapdc  2841  cbvreucsf  3014  reuss2  3303  reuun2  3306  reupick  3307  reupick3  3308  reusn  3541  rabsneu  3543  reuhypd  4330  funcnv3  5121  feu  5241  dff4im  5498  f1ompt  5503  fsn  5524  riotauni  5668  riotacl2  5675  riota1  5680  riota1a  5681  riota2df  5682  snriota  5691  riotaund  5696  acexmid  5705  climreu  10905  divalgb  11417  uptx  12224  txcn  12225  bdcriota  12662