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.36imvOLD
38. 19.36iv
39. 19.37imv
40. 19.37iv
41. 19.41v
42. 19.41vv
43. 19.41vvv
44. 19.41vvvv
45. 19.42v
46. exdistr
47. exdistrv
48. 4exdistrv
49. 19.42vv
50. exdistr2
51. 19.42vvv
52. 3exdistr
53. 4exdistr