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

Definition df-riota 6273
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 5571. (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 6272 . 2  class  ( iota_ x  e.  A  ph )
52cv 1437 . . . . 5  class  x
65, 3wcel 1873 . . . 4  wff  x  e.  A
76, 1wa 371 . . 3  wff  ( x  e.  A  /\  ph )
87, 2cio 5569 . 2  class  ( iota
x ( x  e.  A  /\  ph )
)
94, 8wceq 1438 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  6274  riotabidv  6275  riotaex  6277  riotav  6278  riotauni  6279  nfriota1  6280  nfriotad  6281  cbvriota  6283  csbriota  6285  riotacl2  6286  riotabidva  6289  riota1  6291  riota2df  6293  snriota  6302  riotaund  6308  ismgmid  16512  q1peqb  23109  adjval  27547
  Copyright terms: Public domain W3C validator