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

Definition df-riota 5468
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 4867. (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 5467 . 2  class  ( iota_ x  e.  A  ph )
52cv 1242 . . . . 5  class  x
65, 3wcel 1393 . . . 4  wff  x  e.  A
76, 1wa 97 . . 3  wff  ( x  e.  A  /\  ph )
87, 2cio 4865 . 2  class  ( iota
x ( x  e.  A  /\  ph )
)
94, 8wceq 1243 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  5469  riotabidv  5470  riotaexg  5472  riotav  5473  riotauni  5474  nfriota1  5475  nfriotadxy  5476  cbvriota  5478  riotacl2  5481  riotabidva  5484  riota1  5486  riota2df  5488  snriota  5497  riotaund  5502  bdcriota  9977
  Copyright terms: Public domain W3C validator