MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  df-riota Structured version   Unicode version

Definition df-riota 6267
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 5565. (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 6266 . 2  class  ( iota_ x  e.  A  ph )
52cv 1436 . . . . 5  class  x
65, 3wcel 1870 . . . 4  wff  x  e.  A
76, 1wa 370 . . 3  wff  ( x  e.  A  /\  ph )
87, 2cio 5563 . 2  class  ( iota
x ( x  e.  A  /\  ph )
)
94, 8wceq 1437 1  wff  ( iota_ x  e.  A  ph )  =  ( iota x
( x  e.  A  /\  ph ) )
Colors of variables: wff setvar class
This definition is referenced by:  riotaeqdv  6268  riotabidv  6269  riotaex  6271  riotav  6272  riotauni  6273  nfriota1  6274  nfriotad  6275  cbvriota  6277  csbriota  6279  riotacl2  6280  riotabidva  6283  riota1  6285  riota2df  6287  snriota  6296  riotaund  6302  ismgmid  16458  q1peqb  22980  adjval  27378
  Copyright terms: Public domain W3C validator