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

Definition df-riota 5547
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 4934. (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 5546 . 2  class  ( iota_ x  e.  A  ph )
52cv 1284 . . . . 5  class  x
65, 3wcel 1434 . . . 4  wff  x  e.  A
76, 1wa 102 . . 3  wff  ( x  e.  A  /\  ph )
87, 2cio 4932 . 2  class  ( iota
x ( x  e.  A  /\  ph )
)
94, 8wceq 1285 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  5548  riotabidv  5549  riotaexg  5551  riotav  5552  riotauni  5553  nfriota1  5554  nfriotadxy  5555  cbvriota  5557  riotacl2  5560  riotabidva  5563  riota1  5565  riota2df  5567  snriota  5576  riotaund  5581  bdcriota  11117
  Copyright terms: Public domain W3C validator