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

Definition df-riota 6599
Description: Define restricted description binder. In case it doesn't exist, we return a set which is not a member of the domain of discourse . See also comments for df-iota 5464. (Contributed by NM, 15-Sep-2011.) (Revised by Mario Carneiro, 15-Oct-2016.)
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 6592 . 2
51, 2, 3wreu 2714 . . 3
62cv 1653 . . . . . 6
76, 3wcel 1728 . . . . 5
87, 1wa 360 . . . 4
98, 2cio 5462 . . 3
107, 2cab 2429 . . . 4
11 cund 6591 . . . 4
1210, 11cfv 5501 . . 3
135, 9, 12cif 3765 . 2
144, 13wceq 1654 1
Colors of variables: wff set class
This definition is referenced by:  riotaeqdv  6600  riotabidv  6601  riotaex  6603  riotav  6604  riotaiota  6605  nfriota1  6607  nfriotad  6608  cbvriota  6610  riotabidva  6616  riotaund  6635
  Copyright terms: Public domain W3C validator