Metamath Proof Explorer

Table of Contents - 2.3.14. 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. cbviota
13. cbviotav
14. sb8iota
15. iotaeq
16. iotabi
17. uniabio
18. iotaval
19. iotauni
20. iotaint
21. iota1
22. iotanul
23. iotassuni
24. iotaex
25. iota4
26. iota4an
27. iota5
28. iotabidv
29. iotabii
30. iotacl
31. iota2df
32. iota2d
33. iota2
34. iotan0
35. sniota
36. dfiota4
37. csbiota