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 2915
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 2910 . 2 wff ∃!𝑥𝐴 𝜑
52cv 1479 . . . . 5 class 𝑥
65, 3wcel 1987 . . . 4 wff 𝑥𝐴
76, 1wa 384 . . 3 wff (𝑥𝐴𝜑)
87, 2weu 2469 . 2 wff ∃!𝑥(𝑥𝐴𝜑)
94, 8wb 196 1 wff (∃!𝑥𝐴 𝜑 ↔ ∃!𝑥(𝑥𝐴𝜑))
Colors of variables: wff setvar class
This definition is referenced by:  nfreu1  3104  nfreud  3106  reubida  3117  reubiia  3120  reueq1f  3129  reu5  3152  rmo5  3155  cbvreu  3161  reuv  3211  reu2  3381  reu6  3382  reu3  3383  2reuswap  3397  2reu5lem1  3400  cbvreucsf  3553  reuss2  3889  reuun2  3892  reupick  3893  reupick3  3894  euelss  3896  reusn  4239  rabsneu  4241  reusv2lem4  4842  reusv2lem5  4843  reuhypd  4865  funcnv3  5927  feu  6047  dff4  6339  f1ompt  6348  fsn  6367  riotauni  6582  riotacl2  6589  riota1  6594  riota1a  6595  riota2df  6596  snriota  6606  riotaund  6612  aceq1  8900  dfac2  8913  nqerf  9712  zmin  11744  climreu  14237  divalglem10  15068  divalgb  15070  uptx  21368  txcn  21369  q1peqb  23852  axcontlem2  25779  edgnbusgreu  26190  nbusgredgeu0  26191  frgr3vlem2  27036  3vfriswmgrlem  27039  frgrncvvdeqlem3  27063  frgreu  27083  adjeu  28636  2reuswap2  29217  rmoxfrdOLD  29221  rmoxfrd  29222  neibastop3  32052  poimirlem25  33105  poimirlem27  33107
  Copyright terms: Public domain W3C validator