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

Definition df-riota 5571
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 4948. (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 5570 . 2 class (𝑥𝐴 𝜑)
52cv 1286 . . . . 5 class 𝑥
65, 3wcel 1436 . . . 4 wff 𝑥𝐴
76, 1wa 102 . . 3 wff (𝑥𝐴𝜑)
87, 2cio 4946 . 2 class (℩𝑥(𝑥𝐴𝜑))
94, 8wceq 1287 1 wff (𝑥𝐴 𝜑) = (℩𝑥(𝑥𝐴𝜑))
Colors of variables: wff set class
This definition is referenced by:  riotaeqdv  5572  riotabidv  5573  riotaexg  5575  riotav  5576  riotauni  5577  nfriota1  5578  nfriotadxy  5579  cbvriota  5581  riotacl2  5584  riotabidva  5587  riota1  5589  riota2df  5591  snriota  5600  riotaund  5605  bdcriota  11243
  Copyright terms: Public domain W3C validator