Definition df-reu 2919

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 2914	. 2 wff ∃!𝑥 ∈ 𝐴 𝜑
5	2	cv 1482	. . . . 5 class 𝑥
6	5, 3	wcel 1990	. . . 4 wff 𝑥 ∈ 𝐴
7	6, 1	wa 384	. . 3 wff (𝑥 ∈ 𝐴 ∧ 𝜑)
8	7, 2	weu 2470	. 2 wff ∃!𝑥(𝑥 ∈ 𝐴 ∧ 𝜑)
9	4, 8	wb 196	1 wff (∃!𝑥 ∈ 𝐴 𝜑 ↔ ∃!𝑥(𝑥 ∈ 𝐴 ∧ 𝜑))

This definition is referenced by:  nfreu1  3110  nfreud  3112  reubida  3124  reubiia  3127  reueq1f  3136  reu5  3159  rmo5  3162  reueubd  3164  cbvreu  3169  reuv  3221  reu2  3394  reu6  3395  reu3  3396  2reuswap  3410  2reu5lem1  3413  cbvreucsf  3567  reuss2  3907  reuun2  3910  reupick  3911  reupick3  3912  euelss  3914  reusn  4262  rabsneu  4264  reusv2lem4  4872  reusv2lem5  4873  reuhypd  4895  funcnv3  5959  feu  6080  dff4  6373  f1ompt  6382  fsn  6402  riotauni  6617  riotacl2  6624  riota1  6629  riota1a  6630  riota2df  6631  snriota  6641  riotaund  6647  aceq1  8940  dfac2  8953  nqerf  9752  zmin  11784  climreu  14287  divalglem10  15125  divalgb  15127  uptx  21428  txcn  21429  q1peqb  23914  axcontlem2  25845  edgnbusgreu  26269  nbusgredgeu0  26270  frgr3vlem2  27138  3vfriswmgrlem  27141  frgrncvvdeqlem2  27164  adjeu  28748  2reuswap2  29328  rmoxfrdOLD  29332  rmoxfrd  29333  neibastop3  32357  poimirlem25  33434  poimirlem27  33436