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

Definition df-riota 5389
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 4790. (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 5388 . 2 class (x A φ)
52cv 1225 . . . . 5 class x
65, 3wcel 1370 . . . 4 wff x A
76, 1wa 97 . . 3 wff (x A φ)
87, 2cio 4788 . 2 class (℩x(x A φ))
94, 8wceq 1226 1 wff (x A φ) = (℩x(x A φ))
Colors of variables: wff set class
This definition is referenced by:  riotaeqdv  5390  riotabidv  5391  riotav  5393  riotauni  5394  nfriota1  5395  nfriotadxy  5396  cbvriota  5398  riotacl2  5401  riotabidva  5404  riota1  5406  riota2df  5408  snriota  5417  riotaund  5422  bdcriota  7249
  Copyright terms: Public domain W3C validator