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

Definition df-riota 5830
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 5178. (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 5829 . 2 class (𝑥𝐴 𝜑)
52cv 1352 . . . . 5 class 𝑥
65, 3wcel 2148 . . . 4 wff 𝑥𝐴
76, 1wa 104 . . 3 wff (𝑥𝐴𝜑)
87, 2cio 5176 . 2 class (℩𝑥(𝑥𝐴𝜑))
94, 8wceq 1353 1 wff (𝑥𝐴 𝜑) = (℩𝑥(𝑥𝐴𝜑))
Colors of variables: wff set class
This definition is referenced by:  riotaeqdv  5831  riotabidv  5832  riotaexg  5834  riotav  5835  riotauni  5836  nfriota1  5837  nfriotadxy  5838  cbvriota  5840  riotacl2  5843  riotabidva  5846  riota1  5848  riota2df  5850  snriota  5859  riotaund  5864  grpidvalg  12791  fn0g  12793  ismgmid  12795  oppr1g  13250  bdcriota  14605
  Copyright terms: Public domain W3C validator