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 7107
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 6302. (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 7106 . 2 class (𝑥𝐴 𝜑)
52cv 1537 . . . . 5 class 𝑥
65, 3wcel 2115 . . . 4 wff 𝑥𝐴
76, 1wa 399 . . 3 wff (𝑥𝐴𝜑)
87, 2cio 6300 . 2 class (℩𝑥(𝑥𝐴𝜑))
94, 8wceq 1538 1 wff (𝑥𝐴 𝜑) = (℩𝑥(𝑥𝐴𝜑))
Colors of variables: wff setvar class
This definition is referenced by:  riotaeqdv  7108  riotabidv  7109  riotaex  7111  riotav  7112  riotauni  7113  nfriota1  7114  nfriotadw  7115  cbvriotaw  7116  nfriotad  7118  cbvriota  7120  csbriota  7122  riotacl2  7123  riotabidva  7126  riota1  7128  riota2df  7130  snriota  7140  riotaund  7146  ismgmid  17875  q1peqb  24761  adjval  29679
  Copyright terms: Public domain W3C validator