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

Definition df-riota 5781
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 5136. (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 5780 . 2 class (𝑥𝐴 𝜑)
52cv 1334 . . . . 5 class 𝑥
65, 3wcel 2128 . . . 4 wff 𝑥𝐴
76, 1wa 103 . . 3 wff (𝑥𝐴𝜑)
87, 2cio 5134 . 2 class (℩𝑥(𝑥𝐴𝜑))
94, 8wceq 1335 1 wff (𝑥𝐴 𝜑) = (℩𝑥(𝑥𝐴𝜑))
Colors of variables: wff set class
This definition is referenced by:  riotaeqdv  5782  riotabidv  5783  riotaexg  5785  riotav  5786  riotauni  5787  nfriota1  5788  nfriotadxy  5789  cbvriota  5791  riotacl2  5794  riotabidva  5797  riota1  5799  riota2df  5801  snriota  5810  riotaund  5815  bdcriota  13500
  Copyright terms: Public domain W3C validator