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 7388
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 6514. (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 7387 . 2 class (𝑥𝐴 𝜑)
52cv 1539 . . . . 5 class 𝑥
65, 3wcel 2108 . . . 4 wff 𝑥𝐴
76, 1wa 395 . . 3 wff (𝑥𝐴𝜑)
87, 2cio 6512 . 2 class (℩𝑥(𝑥𝐴𝜑))
94, 8wceq 1540 1 wff (𝑥𝐴 𝜑) = (℩𝑥(𝑥𝐴𝜑))
Colors of variables: wff setvar class
This definition is referenced by:  riotaeqdv  7389  riotabidv  7390  riotaex  7392  riotav  7393  riotauni  7394  nfriota1  7395  nfriotadw  7396  cbvriotaw  7397  cbvriotavw  7398  nfriotad  7399  cbvriota  7401  csbriota  7403  riotacl2  7404  riotabidva  7407  riota1  7409  riota2df  7411  snriota  7421  riotaund  7427  riotarab  7430  ismgmid  18678  q1peqb  26195  adjval  31909  riotaeqbii  36199  cbvriotavw2  36237  cbvriotadavw  36271  cbvriotadavw2  36291
  Copyright terms: Public domain W3C validator