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. iotaval
20. iotauni
21. iotaint
22. iota1
23. iotanul
24. iotassuni
25. iotaex
26. iota4
27. iota4an
28. iota5
29. iotabidv
30. iotabii
31. iotacl
32. iota2df
33. iota2d
34. iota2
35. iotan0
36. sniota
37. dfiota4
38. csbiota