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

Definition df-riota 5696
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 5056. (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 5695 . 2 class (𝑥𝐴 𝜑)
52cv 1313 . . . . 5 class 𝑥
65, 3wcel 1463 . . . 4 wff 𝑥𝐴
76, 1wa 103 . . 3 wff (𝑥𝐴𝜑)
87, 2cio 5054 . 2 class (℩𝑥(𝑥𝐴𝜑))
94, 8wceq 1314 1 wff (𝑥𝐴 𝜑) = (℩𝑥(𝑥𝐴𝜑))
Colors of variables: wff set class
This definition is referenced by:  riotaeqdv  5697  riotabidv  5698  riotaexg  5700  riotav  5701  riotauni  5702  nfriota1  5703  nfriotadxy  5704  cbvriota  5706  riotacl2  5709  riotabidva  5712  riota1  5714  riota2df  5716  snriota  5725  riotaund  5730  bdcriota  12892
  Copyright terms: Public domain W3C validator