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

Definition df-riota 5809
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 5160. (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 5808 . 2 class (𝑥𝐴 𝜑)
52cv 1347 . . . . 5 class 𝑥
65, 3wcel 2141 . . . 4 wff 𝑥𝐴
76, 1wa 103 . . 3 wff (𝑥𝐴𝜑)
87, 2cio 5158 . 2 class (℩𝑥(𝑥𝐴𝜑))
94, 8wceq 1348 1 wff (𝑥𝐴 𝜑) = (℩𝑥(𝑥𝐴𝜑))
Colors of variables: wff set class
This definition is referenced by:  riotaeqdv  5810  riotabidv  5811  riotaexg  5813  riotav  5814  riotauni  5815  nfriota1  5816  nfriotadxy  5817  cbvriota  5819  riotacl2  5822  riotabidva  5825  riota1  5827  riota2df  5829  snriota  5838  riotaund  5843  grpidvalg  12627  fn0g  12629  ismgmid  12631  bdcriota  13918
  Copyright terms: Public domain W3C validator