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

Definition df-riota 5844
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 5190. (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 5843 . 2  class  ( iota_ x  e.  A  ph )
52cv 1362 . . . . 5  class  x
65, 3wcel 2158 . . . 4  wff  x  e.  A
76, 1wa 104 . . 3  wff  ( x  e.  A  /\  ph )
87, 2cio 5188 . 2  class  ( iota
x ( x  e.  A  /\  ph )
)
94, 8wceq 1363 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  5845  riotabidv  5846  riotaexg  5848  riotav  5849  riotauni  5850  nfriota1  5851  nfriotadxy  5852  cbvriota  5854  riotacl2  5857  riotabidva  5860  riota1  5862  riota2df  5864  snriota  5873  riotaund  5878  grpidvalg  12811  fn0g  12813  ismgmid  12815  oppr1g  13330  bdcriota  14931
  Copyright terms: Public domain W3C validator