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

Definition df-riota 6488
Description: Define restricted description binder. In case there is no unique 𝑥 such that (𝑥𝐴𝜑) holds, it evaluates to the empty set. See also comments for df-iota 5753. (Contributed by NM, 15-Sep-2011.) (Revised by Mario Carneiro, 15-Oct-2016.) (Revised by NM, 2-Sep-2018.)
Assertion
Ref Expression
df-riota (𝑥𝐴 𝜑) = (℩𝑥(𝑥𝐴𝜑))

Detailed syntax breakdown of Definition df-riota
StepHypRef Expression
1 wph . . 3 wff 𝜑
2 vx . . 3 setvar 𝑥
3 cA . . 3 class 𝐴
41, 2, 3crio 6487 . 2 class (𝑥𝐴 𝜑)
52cv 1473 . . . . 5 class 𝑥
65, 3wcel 1976 . . . 4 wff 𝑥𝐴
76, 1wa 382 . . 3 wff (𝑥𝐴𝜑)
87, 2cio 5751 . 2 class (℩𝑥(𝑥𝐴𝜑))
94, 8wceq 1474 1 wff (𝑥𝐴 𝜑) = (℩𝑥(𝑥𝐴𝜑))
Colors of variables: wff setvar class
This definition is referenced by:  riotaeqdv  6489  riotabidv  6490  riotaex  6492  riotav  6493  riotauni  6494  nfriota1  6495  nfriotad  6496  cbvriota  6498  csbriota  6500  riotacl2  6501  riotabidva  6504  riota1  6506  riota2df  6508  snriota  6517  riotaund  6523  ismgmid  17035  q1peqb  23662  adjval  27926
  Copyright terms: Public domain W3C validator