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

Definition df-riota 5496
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 4895. (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 5495 . 2 class (𝑥𝐴 𝜑)
52cv 1258 . . . . 5 class 𝑥
65, 3wcel 1409 . . . 4 wff 𝑥𝐴
76, 1wa 101 . . 3 wff (𝑥𝐴𝜑)
87, 2cio 4893 . 2 class (℩𝑥(𝑥𝐴𝜑))
94, 8wceq 1259 1 wff (𝑥𝐴 𝜑) = (℩𝑥(𝑥𝐴𝜑))
Colors of variables: wff set class
This definition is referenced by:  riotaeqdv  5497  riotabidv  5498  riotaexg  5500  riotav  5501  riotauni  5502  nfriota1  5503  nfriotadxy  5504  cbvriota  5506  riotacl2  5509  riotabidva  5512  riota1  5514  riota2df  5516  snriota  5525  riotaund  5530  bdcriota  10390
  Copyright terms: Public domain W3C validator