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

Definition df-riota 6277
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 6276 . 2  class  ( iota_ x  e.  A  ph )
52cv 1454 . . . . 5  class  x
65, 3wcel 1898 . . . 4  wff  x  e.  A
76, 1wa 375 . . 3  wff  ( x  e.  A  /\  ph )
87, 2cio 5563 . 2  class  ( iota
x ( x  e.  A  /\  ph )
)
94, 8wceq 1455 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  6278  riotabidv  6279  riotaex  6281  riotav  6282  riotauni  6283  nfriota1  6284  nfriotad  6285  cbvriota  6287  csbriota  6289  riotacl2  6290  riotabidva  6293  riota1  6295  riota2df  6297  snriota  6306  riotaund  6312  ismgmid  16556  q1peqb  23154  adjval  27592
  Copyright terms: Public domain W3C validator