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

Definition df-riota 5411
Description: Define restricted description binder. In case there is no unique x such that (x A φ) holds, it evaluates to the empty set. See also comments for df-iota 4810. (Contributed by NM, 15-Sep-2011.) (Revised by Mario Carneiro, 15-Oct-2016.) (Revised by NM, 2-Sep-2018.)
Assertion
Ref Expression
df-riota (x A φ) = (℩x(x A φ))

Detailed syntax breakdown of Definition df-riota
StepHypRef Expression
1 wph . . 3 wff φ
2 vx . . 3 setvar x
3 cA . . 3 class A
41, 2, 3crio 5410 . 2 class (x A φ)
52cv 1241 . . . . 5 class x
65, 3wcel 1390 . . . 4 wff x A
76, 1wa 97 . . 3 wff (x A φ)
87, 2cio 4808 . 2 class (℩x(x A φ))
94, 8wceq 1242 1 wff (x A φ) = (℩x(x A φ))
Colors of variables: wff set class
This definition is referenced by:  riotaeqdv  5412  riotabidv  5413  riotaexg  5415  riotav  5416  riotauni  5417  nfriota1  5418  nfriotadxy  5419  cbvriota  5421  riotacl2  5424  riotabidva  5427  riota1  5429  riota2df  5431  snriota  5440  riotaund  5445  bdcriota  9272
  Copyright terms: Public domain W3C validator