Metamath Proof Explorer

Table of Contents - 1.4.4. Axiom scheme ax-5 (Distinctness) - first use of $d

  1. ax-5
  2. ax5d
  3. ax5e
  4. ax5ea
  5. nfv
  6. nfvd
  7. alimdv
  8. eximdv
  9. 2alimdv
  10. 2eximdv
  11. albidv
  12. exbidv
  13. nfbidv
  14. 2albidv
  15. 2exbidv
  16. 3exbidv
  17. 4exbidv
  18. alrimiv
  19. alrimivv
  20. alrimdv
  21. exlimiv
  22. exlimiiv
  23. exlimivv
  24. exlimdv
  25. exlimdvv
  26. exlimddv
  27. nexdv
  28. 2ax5
  29. stdpc5v
  30. 19.21v
  31. 19.32v
  32. 19.31v
  33. 19.23v
  34. 19.23vv
  35. pm11.53v
  36. 19.36imv
  37. 19.36iv
  38. 19.37imv
  39. 19.37iv
  40. 19.41v
  41. 19.41vv
  42. 19.41vvv
  43. 19.41vvvv
  44. 19.42v
  45. exdistr
  46. exdistrv
  47. 4exdistrv
  48. 19.42vv
  49. exdistr2
  50. 19.42vvv
  51. 19.42vvvOLD
  52. 3exdistr
  53. 4exdistr