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