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. iotavalOLD
25. iotauni
26. iotaint
27. iota1
28. iotanul
29. iotassuniOLD
30. iotaexOLD
31. iota4
32. iota4an
33. iota5
34. iotabidv
35. iotabii
36. iotacl
37. iota2df
38. iota2d
39. iota2
40. iotan0
41. sniota
42. dfiota4
43. csbiota