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 6831
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 6060. (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 6830 . 2 class (𝑥𝐴 𝜑)
52cv 1636 . . . . 5 class 𝑥
65, 3wcel 2156 . . . 4 wff 𝑥𝐴
76, 1wa 384 . . 3 wff (𝑥𝐴𝜑)
87, 2cio 6058 . 2 class (℩𝑥(𝑥𝐴𝜑))
94, 8wceq 1637 1 wff (𝑥𝐴 𝜑) = (℩𝑥(𝑥𝐴𝜑))
Colors of variables: wff setvar class
This definition is referenced by:  riotaeqdv  6832  riotabidv  6833  riotaex  6835  riotav  6836  riotauni  6837  nfriota1  6838  nfriotad  6839  cbvriota  6841  csbriota  6843  riotacl2  6844  riotabidva  6847  riota1  6849  riota2df  6851  snriota  6861  riotaund  6867  ismgmid  17465  q1peqb  24124  adjval  29073
  Copyright terms: Public domain W3C validator