Metamath Proof Explorer

Table of Contents - 21.13.2. Change bound variables.

1. in-ax8
2. ss-ax8
3. Change bound variables and domains.
   1. cbvralvw2
   2. cbvrexvw2
   3. cbvrmovw2
   4. cbvreuvw2
   5. cbvsbcvw2
   6. cbvcsbvw2
   7. cbviunvw2
   8. cbviinvw2
   9. cbvmptvw2
   10. cbvdisjvw2
   11. cbvriotavw2
   12. cbvoprab1vw
   13. cbvoprab2vw
   14. cbvoprab123vw
   15. cbvoprab23vw
   16. cbvoprab13vw
   17. cbvmpovw2
   18. cbvmpo1vw2
   19. cbvmpo2vw2
   20. cbvixpvw2
   21. cbvsumvw2
   22. cbvprodvw2
   23. cbvitgvw2
   24. cbvditgvw2
4. Change bound variables, deduction versions.
   1. cbvmodavw
   2. cbveudavw
   3. cbvrmodavw
   4. cbvreudavw
   5. cbvsbdavw
   6. cbvsbdavw2
   7. cbvabdavw
   8. cbvsbcdavw
   9. cbvsbcdavw2
   10. cbvcsbdavw
   11. cbvcsbdavw2
   12. cbvrabdavw
   13. cbviundavw
   14. cbviindavw
   15. cbvopab1davw
   16. cbvopab2davw
   17. cbvopabdavw
   18. cbvmptdavw
   19. cbvdisjdavw
   20. cbviotadavw
   21. cbvriotadavw
   22. cbvoprab1davw
   23. cbvoprab2davw
   24. cbvoprab3davw
   25. cbvoprab123davw
   26. cbvoprab12davw
   27. cbvoprab23davw
   28. cbvoprab13davw
   29. cbvixpdavw
   30. cbvsumdavw
   31. cbvproddavw
   32. cbvitgdavw
   33. cbvditgdavw
5. Change bound variables and domains, deduction versions.
   1. cbvrmodavw2
   2. cbvreudavw2
   3. cbvrabdavw2
   4. cbviundavw2
   5. cbviindavw2
   6. cbvmptdavw2
   7. cbvdisjdavw2
   8. cbvriotadavw2
   9. cbvmpodavw2
   10. cbvmpo1davw2
   11. cbvmpo2davw2
   12. cbvixpdavw2
   13. cbvsumdavw2
   14. cbvproddavw2
   15. cbvitgdavw2
   16. cbvditgdavw2