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 6772
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 6010. (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 6771 . 2 class (𝑥𝐴 𝜑)
52cv 1629 . . . . 5 class 𝑥
65, 3wcel 2137 . . . 4 wff 𝑥𝐴
76, 1wa 383 . . 3 wff (𝑥𝐴𝜑)
87, 2cio 6008 . 2 class (℩𝑥(𝑥𝐴𝜑))
94, 8wceq 1630 1 wff (𝑥𝐴 𝜑) = (℩𝑥(𝑥𝐴𝜑))
Colors of variables: wff setvar class
This definition is referenced by:  riotaeqdv  6773  riotabidv  6774  riotaex  6776  riotav  6777  riotauni  6778  nfriota1  6779  nfriotad  6780  cbvriota  6782  csbriota  6784  riotacl2  6785  riotabidva  6788  riota1  6790  riota2df  6792  snriota  6802  riotaund  6808  ismgmid  17463  q1peqb  24111  adjval  29056
  Copyright terms: Public domain W3C validator