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 7375
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 6501. (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 7374 . 2 class (𝑥𝐴 𝜑)
52cv 1532 . . . . 5 class 𝑥
65, 3wcel 2098 . . . 4 wff 𝑥𝐴
76, 1wa 394 . . 3 wff (𝑥𝐴𝜑)
87, 2cio 6499 . 2 class (℩𝑥(𝑥𝐴𝜑))
94, 8wceq 1533 1 wff (𝑥𝐴 𝜑) = (℩𝑥(𝑥𝐴𝜑))
Colors of variables: wff setvar class
This definition is referenced by:  riotaeqdv  7376  riotabidv  7377  riotaex  7379  riotav  7380  riotauni  7381  nfriota1  7382  nfriotadw  7383  cbvriotaw  7384  cbvriotavw  7385  nfriotad  7387  cbvriota  7389  csbriota  7391  riotacl2  7392  riotabidva  7395  riota1  7397  riota2df  7399  snriota  7409  riotaund  7415  riotarab  7418  ismgmid  18628  q1peqb  26136  adjval  31772
  Copyright terms: Public domain W3C validator