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 3049
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 3044 . 2 wff ∃!𝑥𝐴 𝜑
52cv 1623 . . . . 5 class 𝑥
65, 3wcel 2131 . . . 4 wff 𝑥𝐴
76, 1wa 383 . . 3 wff (𝑥𝐴𝜑)
87, 2weu 2599 . 2 wff ∃!𝑥(𝑥𝐴𝜑)
94, 8wb 196 1 wff (∃!𝑥𝐴 𝜑 ↔ ∃!𝑥(𝑥𝐴𝜑))
Colors of variables: wff setvar class
This definition is referenced by:  nfreu1  3240  nfreud  3242  reubida  3255  reubiia  3258  reueq1f  3267  reu5  3290  rmo5  3293  reueubd  3295  cbvreu  3300  reuv  3353  reu2  3527  reu6  3528  reu3  3529  2reuswap  3543  2reu5lem1  3546  cbvreucsf  3700  reuss2  4042  reuun2  4045  reupick  4046  reupick3  4047  euelss  4049  reusn  4398  rabsneu  4400  reusv2lem4  5013  reusv2lem5  5014  reuhypd  5036  funcnv3  6112  feu  6233  dff4  6528  f1ompt  6537  fsn  6557  riotauni  6772  riotacl2  6779  riota1  6784  riota1a  6785  riota2df  6786  snriota  6796  riotaund  6802  aceq1  9122  dfac2b  9135  dfac2OLD  9137  nqerf  9936  zmin  11969  climreu  14478  divalglem10  15319  divalgb  15321  uptx  21622  txcn  21623  q1peqb  24105  axcontlem2  26036  edgnbusgreu  26459  nbusgredgeu0  26460  frgr3vlem2  27420  3vfriswmgrlem  27423  frgrncvvdeqlem2  27446  adjeu  29049  2reuswap2  29628  rmoxfrdOLD  29632  rmoxfrd  29633  neibastop3  32655  poimirlem25  33739  poimirlem27  33741
  Copyright terms: Public domain W3C validator