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

Definition df-riota 5698
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 5058. (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 5697 . 2  class  ( iota_ x  e.  A  ph )
52cv 1315 . . . . 5  class  x
65, 3wcel 1465 . . . 4  wff  x  e.  A
76, 1wa 103 . . 3  wff  ( x  e.  A  /\  ph )
87, 2cio 5056 . 2  class  ( iota
x ( x  e.  A  /\  ph )
)
94, 8wceq 1316 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  5699  riotabidv  5700  riotaexg  5702  riotav  5703  riotauni  5704  nfriota1  5705  nfriotadxy  5706  cbvriota  5708  riotacl2  5711  riotabidva  5714  riota1  5716  riota2df  5718  snriota  5727  riotaund  5732  bdcriota  12977
  Copyright terms: Public domain W3C validator