Metamath Proof Explorer

Table of Contents - 2.3.15. Definite description binder (inverted iota)

1. cio
2. iotajust
3. df-iota
4. dfiota2
5. nfiota1
6. nfiotadw
7. nfiotaw
8. nfiotad
9. nfiota
10. cbviotaw
11. cbviotavw
12. cbviotavwOLD
13. cbviota
14. cbviotav
15. sb8iota
16. iotaeq
17. iotabi
18. uniabio
19. iotaval2
20. iotauni2
21. iotanul2
22. iotaval
23. iotassuni
24. iotaex
25. iotavalOLD
26. iotauni
27. iotaint
28. iota1
29. iotanul
30. iotassuniOLD
31. iotaexOLD
32. iota4
33. iota4an
34. iota5
35. iotabidv
36. iotabii
37. iotacl
38. iota2df
39. iota2d
40. iota2
41. iotan0
42. sniota
43. dfiota4
44. csbiota