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 7103
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 6308. (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 7102 . 2 class (𝑥𝐴 𝜑)
52cv 1527 . . . . 5 class 𝑥
65, 3wcel 2105 . . . 4 wff 𝑥𝐴
76, 1wa 396 . . 3 wff (𝑥𝐴𝜑)
87, 2cio 6306 . 2 class (℩𝑥(𝑥𝐴𝜑))
94, 8wceq 1528 1 wff (𝑥𝐴 𝜑) = (℩𝑥(𝑥𝐴𝜑))
Colors of variables: wff setvar class
This definition is referenced by:  riotaeqdv  7104  riotabidv  7105  riotaex  7107  riotav  7108  riotauni  7109  nfriota1  7110  nfriotadw  7111  cbvriotaw  7112  nfriotad  7114  cbvriota  7116  csbriota  7118  riotacl2  7119  riotabidva  7122  riota1  7124  riota2df  7126  snriota  7136  riotaund  7142  ismgmid  17865  q1peqb  24677  adjval  29595
  Copyright terms: Public domain W3C validator