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 6576
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 5820. (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 6575 . 2 class (𝑥𝐴 𝜑)
52cv 1479 . . . . 5 class 𝑥
65, 3wcel 1987 . . . 4 wff 𝑥𝐴
76, 1wa 384 . . 3 wff (𝑥𝐴𝜑)
87, 2cio 5818 . 2 class (℩𝑥(𝑥𝐴𝜑))
94, 8wceq 1480 1 wff (𝑥𝐴 𝜑) = (℩𝑥(𝑥𝐴𝜑))
Colors of variables: wff setvar class
This definition is referenced by:  riotaeqdv  6577  riotabidv  6578  riotaex  6580  riotav  6581  riotauni  6582  nfriota1  6583  nfriotad  6584  cbvriota  6586  csbriota  6588  riotacl2  6589  riotabidva  6592  riota1  6594  riota2df  6596  snriota  6606  riotaund  6612  ismgmid  17204  q1peqb  23852  adjval  28637
  Copyright terms: Public domain W3C validator