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

Definition df-riota 5569
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 4946. (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 5568 . 2  class  ( iota_ x  e.  A  ph )
52cv 1286 . . . . 5  class  x
65, 3wcel 1436 . . . 4  wff  x  e.  A
76, 1wa 102 . . 3  wff  ( x  e.  A  /\  ph )
87, 2cio 4944 . 2  class  ( iota
x ( x  e.  A  /\  ph )
)
94, 8wceq 1287 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  5570  riotabidv  5571  riotaexg  5573  riotav  5574  riotauni  5575  nfriota1  5576  nfriotadxy  5577  cbvriota  5579  riotacl2  5582  riotabidva  5585  riota1  5587  riota2df  5589  snriota  5598  riotaund  5603  bdcriota  11219
  Copyright terms: Public domain W3C validator