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

Definition df-riota 5831
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 5179. (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 5830 . 2 class (𝑥𝐴 𝜑)
52cv 1352 . . . . 5 class 𝑥
65, 3wcel 2148 . . . 4 wff 𝑥𝐴
76, 1wa 104 . . 3 wff (𝑥𝐴𝜑)
87, 2cio 5177 . 2 class (℩𝑥(𝑥𝐴𝜑))
94, 8wceq 1353 1 wff (𝑥𝐴 𝜑) = (℩𝑥(𝑥𝐴𝜑))
Colors of variables: wff set class
This definition is referenced by:  riotaeqdv  5832  riotabidv  5833  riotaexg  5835  riotav  5836  riotauni  5837  nfriota1  5838  nfriotadxy  5839  cbvriota  5841  riotacl2  5844  riotabidva  5847  riota1  5849  riota2df  5851  snriota  5860  riotaund  5865  grpidvalg  12792  fn0g  12794  ismgmid  12796  oppr1g  13252  bdcriota  14638
  Copyright terms: Public domain W3C validator