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

Definition df-riota 6062
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 5401. (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 6061 . 2
52cv 1669 . . . . 5
65, 3wcel 1732 . . . 4
76, 1wa 360 . . 3
87, 2cio 5399 . 2
94, 8wceq 1670 1
Colors of variables: wff set class
This definition is referenced by:  riotaeqdv  6063  riotabidv  6064  riotaex  6066  riotav  6067  riotaiotaOLD  6068  riotauni  6069  nfriota1  6070  nfriotad  6071  cbvriota  6073  csbriota  6075  riotacl2  6077  riotabidva  6080  riota1  6082  riota2df  6084  snriota  6093  riotaund  6099  riotaprcOLD  6100  ismgmid  15276  q1peqb  21092  adjval  24416
  Copyright terms: Public domain W3C validator