Definition df-reu 2475

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

This definition is referenced by:  nfreu1  2662  nfreudxy  2664  reubida  2672  reubiia  2675  reueq1f  2684  reu5  2703  rmo5  2706  cbvreu  2716  cbvreuvw  2724  reuv  2771  reu2  2940  reu6  2941  reu3  2942  2reuswapdc  2956  cbvreucsf  3136  reuss2  3430  reuun2  3433  reupick  3434  reupick3  3435  reusn  3678  rabsneu  3680  reuhypd  4489  funcnv3  5297  feu  5417  dff4im  5683  f1ompt  5688  fsn  5709  riotauni  5859  riotacl2  5866  riota1  5871  riota1a  5872  riota2df  5873  snriota  5882  riotaund  5887  acexmid  5896  climreu  11340  divalgb  11965  uptx  14251  txcn  14252  dedekindicc  14588  bdcriota  15113