ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  df-riota GIF version

Definition df-riota 5698
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 5058. (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 5697 . 2 class (𝑥𝐴 𝜑)
52cv 1315 . . . . 5 class 𝑥
65, 3wcel 1465 . . . 4 wff 𝑥𝐴
76, 1wa 103 . . 3 wff (𝑥𝐴𝜑)
87, 2cio 5056 . 2 class (℩𝑥(𝑥𝐴𝜑))
94, 8wceq 1316 1 wff (𝑥𝐴 𝜑) = (℩𝑥(𝑥𝐴𝜑))
Colors of variables: wff set class
This definition is referenced by:  riotaeqdv  5699  riotabidv  5700  riotaexg  5702  riotav  5703  riotauni  5704  nfriota1  5705  nfriotadxy  5706  cbvriota  5708  riotacl2  5711  riotabidva  5714  riota1  5716  riota2df  5718  snriota  5727  riotaund  5732  bdcriota  12977
  Copyright terms: Public domain W3C validator