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

Definition df-riota 5495
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 4894. (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 5494 . 2  class  ( iota_ x  e.  A  ph )
52cv 1258 . . . . 5  class  x
65, 3wcel 1409 . . . 4  wff  x  e.  A
76, 1wa 101 . . 3  wff  ( x  e.  A  /\  ph )
87, 2cio 4892 . 2  class  ( iota
x ( x  e.  A  /\  ph )
)
94, 8wceq 1259 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  5496  riotabidv  5497  riotaexg  5499  riotav  5500  riotauni  5501  nfriota1  5502  nfriotadxy  5503  cbvriota  5505  riotacl2  5508  riotabidva  5511  riota1  5513  riota2df  5515  snriota  5524  riotaund  5529  bdcriota  10369
  Copyright terms: Public domain W3C validator