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 6937
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 6152. (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 6936 . 2 class (𝑥𝐴 𝜑)
52cv 1506 . . . . 5 class 𝑥
65, 3wcel 2050 . . . 4 wff 𝑥𝐴
76, 1wa 387 . . 3 wff (𝑥𝐴𝜑)
87, 2cio 6150 . 2 class (℩𝑥(𝑥𝐴𝜑))
94, 8wceq 1507 1 wff (𝑥𝐴 𝜑) = (℩𝑥(𝑥𝐴𝜑))
Colors of variables: wff setvar class
This definition is referenced by:  riotaeqdv  6938  riotabidv  6939  riotaex  6941  riotav  6942  riotauni  6943  nfriota1  6944  nfriotad  6945  cbvriota  6947  csbriota  6949  riotacl2  6950  riotabidva  6953  riota1  6955  riota2df  6957  snriota  6967  riotaund  6973  ismgmid  17732  q1peqb  24451  adjval  29448
  Copyright terms: Public domain W3C validator