Definition df-reu 2902

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 2897	. 2 wff ∃!𝑥 ∈ 𝐴 𝜑
5	2	cv 1473	. . . . 5 class 𝑥
6	5, 3	wcel 1976	. . . 4 wff 𝑥 ∈ 𝐴
7	6, 1	wa 382	. . 3 wff (𝑥 ∈ 𝐴 ∧ 𝜑)
8	7, 2	weu 2457	. 2 wff ∃!𝑥(𝑥 ∈ 𝐴 ∧ 𝜑)
9	4, 8	wb 194	1 wff (∃!𝑥 ∈ 𝐴 𝜑 ↔ ∃!𝑥(𝑥 ∈ 𝐴 ∧ 𝜑))

This definition is referenced by:  nfreu1  3088  nfreud  3090  reubida  3100  reubiia  3103  reueq1f  3112  reu5  3135  rmo5  3138  cbvreu  3144  reuv  3193  reu2  3360  reu6  3361  reu3  3362  2reuswap  3376  2reu5lem1  3379  cbvreucsf  3532  reuss2  3865  reuun2  3868  reupick  3869  reupick3  3870  euelss  3872  reusn  4205  rabsneu  4207  reusv2lem4  4792  reusv2lem5  4793  reuhypd  4815  funcnv3  5858  feu  5977  dff4  6265  f1ompt  6274  fsn  6292  riotauni  6494  riotacl2  6501  riota1  6506  riota1a  6507  riota2df  6508  snriota  6517  riotaund  6523  aceq1  8800  dfac2  8813  nqerf  9608  zmin  11618  climreu  14083  divalglem10  14911  divalgb  14913  uptx  21185  txcn  21186  q1peqb  23662  axcontlem2  25590  frgra3vlem2  26321  3vfriswmgralem  26324  frgrancvvdeqlem3  26352  frgraeu  26374  adjeu  27925  2reuswap2  28505  rmoxfrdOLD  28509  rmoxfrd  28510  neibastop3  31320  poimirlem25  32387  poimirlem27  32389  edgnbusgreu  40576  nbusgredgeu0  40577  frgr3vlem2  41425  3vfriswmgrlem  41428  frgrncvvdeqlem3  41452  frgreu  41472