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

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

Detailed syntax breakdown of Definition df-riota
StepHypRef Expression
1 wph . . 3  wff  ph
2 vx . . 3  setvar  x
3 cA . . 3  class  A
41, 2, 3crio 5661 . 2  class  ( iota_ x  e.  A  ph )
52cv 1298 . . . . 5  class  x
65, 3wcel 1448 . . . 4  wff  x  e.  A
76, 1wa 103 . . 3  wff  ( x  e.  A  /\  ph )
87, 2cio 5022 . 2  class  ( iota
x ( x  e.  A  /\  ph )
)
94, 8wceq 1299 1  wff  ( iota_ x  e.  A  ph )  =  ( iota x
( x  e.  A  /\  ph ) )
Colors of variables: wff set class
This definition is referenced by:  riotaeqdv  5663  riotabidv  5664  riotaexg  5666  riotav  5667  riotauni  5668  nfriota1  5669  nfriotadxy  5670  cbvriota  5672  riotacl2  5675  riotabidva  5678  riota1  5680  riota2df  5682  snriota  5691  riotaund  5696  bdcriota  12662
  Copyright terms: Public domain W3C validator