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

Definition df-riota 6232
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 5534. (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 6231 . 2  class  ( iota_ x  e.  A  ph )
52cv 1397 . . . . 5  class  x
65, 3wcel 1823 . . . 4  wff  x  e.  A
76, 1wa 367 . . 3  wff  ( x  e.  A  /\  ph )
87, 2cio 5532 . 2  class  ( iota
x ( x  e.  A  /\  ph )
)
94, 8wceq 1398 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  6233  riotabidv  6234  riotaex  6236  riotav  6237  riotauni  6238  nfriota1  6239  nfriotad  6240  cbvriota  6242  csbriota  6244  riotacl2  6245  riotabidva  6248  riota1  6250  riota2df  6252  snriota  6261  riotaund  6267  ismgmid  16093  q1peqb  22724  adjval  27010
  Copyright terms: Public domain W3C validator