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 2948
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 2943 . 2 wff ∃!𝑥𝐴 𝜑
52cv 1522 . . . . 5 class 𝑥
65, 3wcel 2030 . . . 4 wff 𝑥𝐴
76, 1wa 383 . . 3 wff (𝑥𝐴𝜑)
87, 2weu 2498 . 2 wff ∃!𝑥(𝑥𝐴𝜑)
94, 8wb 196 1 wff (∃!𝑥𝐴 𝜑 ↔ ∃!𝑥(𝑥𝐴𝜑))
Colors of variables: wff setvar class
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
  Copyright terms: Public domain W3C validator