Metamath Proof Explorer

Table of Contents - 2.3.9. Founded and well-ordering relations

1. wfr
2. wse
3. wwe
4. df-fr
5. df-se
6. df-we
7. dffr6
8. frd
9. fri
10. friOLD
11. seex
12. exse
13. dffr2
14. dffr2ALT
15. frc
16. frss
17. sess1
18. sess2
19. freq1
20. freq2
21. seeq1
22. seeq2
23. nffr
24. nfse
25. nfwe
26. frirr
27. fr2nr
28. fr0
29. frminex
30. efrirr
31. efrn2lp
32. epse
33. tz7.2
34. dfepfr
35. epfrc
36. wess
37. weeq1
38. weeq2
39. wefr
40. weso
41. wecmpep
42. wetrep
43. wefrc
44. we0
45. wereu
46. wereu2