MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  df-reu Structured version   Visualization version   GIF version

Definition df-reu 3103
Description: Define restricted existential uniqueness. (Contributed by NM, 22-Nov-1994.)
Assertion
Ref Expression
df-reu (∃!𝑥𝐴 𝜑 ↔ ∃!𝑥(𝑥𝐴𝜑))

Detailed syntax breakdown of Definition df-reu
StepHypRef Expression
1 wph . . 3 wff 𝜑
2 vx . . 3 setvar 𝑥
3 cA . . 3 class 𝐴
41, 2, 3wreu 3098 . 2 wff ∃!𝑥𝐴 𝜑
52cv 1636 . . . . 5 class 𝑥
65, 3wcel 2156 . . . 4 wff 𝑥𝐴
76, 1wa 384 . . 3 wff (𝑥𝐴𝜑)
87, 2weu 2630 . 2 wff ∃!𝑥(𝑥𝐴𝜑)
94, 8wb 197 1 wff (∃!𝑥𝐴 𝜑 ↔ ∃!𝑥(𝑥𝐴𝜑))
Colors of variables: wff setvar class
This definition is referenced by:  reuanid  3108  nfreu1  3298  nfreud  3300  reubida  3313  reubiia  3316  reueq1f  3325  reu5  3348  rmo5  3351  reueubd  3353  cbvreu  3358  reuv  3415  reu2  3592  reu6  3593  reu3  3594  2reuswap  3608  2reu5lem1  3611  cbvreucsf  3762  reuss2  4108  reuun2  4111  reupick  4112  reupick3  4113  euelss  4115  reusn  4453  rabsneu  4455  reusv2lem4  5070  reusv2lem5  5071  reuhypd  5092  funcnv3  6166  feu  6291  dff4  6591  f1ompt  6599  fsn  6621  riotauni  6837  riotacl2  6844  riota1  6849  riota1a  6850  riota2df  6851  snriota  6861  riotaund  6867  aceq1  9219  dfac2b  9232  dfac2OLD  9234  nqerf  10033  zmin  11999  climreu  14506  divalglem10  15341  divalgb  15343  uptx  21638  txcn  21639  q1peqb  24124  axcontlem2  26055  edgnbusgreu  26480  edgnbusgreuOLD  26481  nbusgredgeu0  26482  frgr3vlem2  27445  3vfriswmgrlem  27448  frgrncvvdeqlem2  27471  adjeu  29072  2reuswap2  29650  rmoxfrdOLD  29654  rmoxfrd  29655  neibastop3  32673  poimirlem25  33742  poimirlem27  33744
  Copyright terms: Public domain W3C validator