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

Definition df-riota 6052
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 5381. (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 6051 . 2
52cv 1368 . . . . 5
65, 3wcel 1756 . . . 4
76, 1wa 369 . . 3
87, 2cio 5379 . 2
94, 8wceq 1369 1
Colors of variables: wff setvar class
This definition is referenced by:  riotaeqdv  6053  riotabidv  6054  riotaex  6056  riotav  6057  riotauni  6058  nfriota1  6059  nfriotad  6060  cbvriota  6062  csbriota  6064  riotacl2  6066  riotabidva  6069  riota1  6071  riota2df  6073  snriota  6082  riotaund  6088  ismgmid  15435  q1peqb  21626  adjval  25294
  Copyright terms: Public domain W3C validator