Metamath Proof Explorer

Table of Contents - 1.4.8. Define proper substitution

1. sbjust
2. wsb
3. df-sb
4. dfsb
5. sbtlem
6. sbt
7. sbtru
8. stdpc4
9. sbtALT
10. 2stdpc4
11. sbi1
12. spsbim
13. spsbbi
14. sbimi
15. sb2imi
16. sbbii
17. 2sbbii
18. sbimdv
19. sbbidv
20. sban
21. sb3an
22. spsbe
23. sbequ
24. sbequi
25. sb6
26. 2sb6
27. sb1v
28. sbv
29. sbcom4
30. pm11.07
31. sbrimvw
32. sbbiiev
33. sbievw
34. sbievwOLD
35. sbiedvw
36. 2sbievw
37. sbcom3vv
38. sbievw2
39. sbco2vv
40. cbvsbv
41. sbco4lem
42. sbco4
43. equsb3
44. equsb3r
45. equsb1v
46. nsb
47. sbn1