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

Definition df-riota 6242
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 5541. (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 6241 . 2  class  ( iota_ x  e.  A  ph )
52cv 1382 . . . . 5  class  x
65, 3wcel 1804 . . . 4  wff  x  e.  A
76, 1wa 369 . . 3  wff  ( x  e.  A  /\  ph )
87, 2cio 5539 . 2  class  ( iota
x ( x  e.  A  /\  ph )
)
94, 8wceq 1383 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  6243  riotabidv  6244  riotaex  6246  riotav  6247  riotauni  6248  nfriota1  6249  nfriotad  6250  cbvriota  6252  csbriota  6254  riotacl2  6256  riotabidva  6259  riota1  6261  riota2df  6263  snriota  6272  riotaund  6278  ismgmid  15870  q1peqb  22533  adjval  26787
  Copyright terms: Public domain W3C validator