Definition df-reu 2948

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 2943	. 2 wff ∃!𝑥 ∈ 𝐴 𝜑
5	2	cv 1522	. . . . 5 class 𝑥
6	5, 3	wcel 2030	. . . 4 wff 𝑥 ∈ 𝐴
7	6, 1	wa 383	. . 3 wff (𝑥 ∈ 𝐴 ∧ 𝜑)
8	7, 2	weu 2498	. 2 wff ∃!𝑥(𝑥 ∈ 𝐴 ∧ 𝜑)
9	4, 8	wb 196	1 wff (∃!𝑥 ∈ 𝐴 𝜑 ↔ ∃!𝑥(𝑥 ∈ 𝐴 ∧ 𝜑))

This definition is referenced by:  nfreu1  3139  nfreud  3141  reubida  3154  reubiia  3157  reueq1f  3166  reu5  3189  rmo5  3192  reueubd  3194  cbvreu  3199  reuv  3252  reu2  3427  reu6  3428  reu3  3429  2reuswap  3443  2reu5lem1  3446  cbvreucsf  3600  reuss2  3940  reuun2  3943  reupick  3944  reupick3  3945  euelss  3947  reusn  4294  rabsneu  4296  reusv2lem4  4902  reusv2lem5  4903  reuhypd  4925  funcnv3  5997  feu  6118  dff4  6413  f1ompt  6422  fsn  6442  riotauni  6657  riotacl2  6664  riota1  6669  riota1a  6670  riota2df  6671  snriota  6681  riotaund  6687  aceq1  8978  dfac2  8991  nqerf  9790  zmin  11822  climreu  14331  divalglem10  15172  divalgb  15174  uptx  21476  txcn  21477  q1peqb  23959  axcontlem2  25890  edgnbusgreu  26313  nbusgredgeu0  26314  frgr3vlem2  27254  3vfriswmgrlem  27257  frgrncvvdeqlem2  27280  adjeu  28876  2reuswap2  29455  rmoxfrdOLD  29459  rmoxfrd  29460  neibastop3  32482  poimirlem25  33564  poimirlem27  33566