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

Definition df-riota 6257
Description: Define restricted description binder. In case there is no unique such that holds, it evaluates to the empty set. See also comments for df-iota 5556. (Contributed by NM, 15-Sep-2011.) (Revised by Mario Carneiro, 15-Oct-2016.) (Revised by NM, 2-Sep-2018.)
Assertion
Ref Expression
df-riota

Detailed syntax breakdown of Definition df-riota
StepHypRef Expression
1 wph . . 3
2 vx . . 3
3 cA . . 3
41, 2, 3crio 6256 . 2
52cv 1394 . . . . 5
65, 3wcel 1818 . . . 4
76, 1wa 369 . . 3
87, 2cio 5554 . 2
94, 8wceq 1395 1
Colors of variables: wff setvar class
This definition is referenced by:  riotaeqdv  6258  riotabidv  6259  riotaex  6261  riotav  6262  riotauni  6263  nfriota1  6264  nfriotad  6265  cbvriota  6267  csbriota  6269  riotacl2  6271  riotabidva  6274  riota1  6276  riota2df  6278  snriota  6287  riotaund  6293  ismgmid  15891  q1peqb  22555  adjval  26809
  Copyright terms: Public domain W3C validator