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

Definition df-riota 5468
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 4867. (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 5467 . 2 class (𝑥𝐴 𝜑)
52cv 1242 . . . . 5 class 𝑥
65, 3wcel 1393 . . . 4 wff 𝑥𝐴
76, 1wa 97 . . 3 wff (𝑥𝐴𝜑)
87, 2cio 4865 . 2 class (℩𝑥(𝑥𝐴𝜑))
94, 8wceq 1243 1 wff (𝑥𝐴 𝜑) = (℩𝑥(𝑥𝐴𝜑))
Colors of variables: wff set class
This definition is referenced by:  riotaeqdv  5469  riotabidv  5470  riotaexg  5472  riotav  5473  riotauni  5474  nfriota1  5475  nfriotadxy  5476  cbvriota  5478  riotacl2  5481  riotabidva  5484  riota1  5486  riota2df  5488  snriota  5497  riotaund  5502  bdcriota  9976
  Copyright terms: Public domain W3C validator