Metamath Proof Explorer

Table of Contents - 20.43.1. General auxiliary theorems (1)

1. Unordered and ordered pairs - extension for singletons
   1. eusnsn
   2. absnsb
   3. euabsneu
2. Unordered and ordered pairs - extension for unordered pairs
   1. elprneb
3. Unordered and ordered pairs - extension for ordered pairs
   1. oppr
   2. opprb
   3. or2expropbilem1
   4. or2expropbilem2
   5. or2expropbi
4. Relations - extension
   1. eubrv
   2. eubrdm
   3. eldmressn
5. Definite description binder (inverted iota) - extension
   1. iota0def
   2. iota0ndef
6. Functions - extension
   1. fveqvfvv
   2. fnresfnco
   3. funcoressn
   4. funressnfv
   5. funressndmfvrn
   6. funressnvmo
   7. funressnmo
   8. funressneu
   9. fresfo
   10. fsetsniunop
   11. fsetabsnop
   12. fsetsnf
   13. fsetsnf1
   14. fsetsnfo
   15. fsetsnf1o
   16. fsetsnprcnex
   17. cfsetssfset
   18. cfsetsnfsetfv
   19. cfsetsnfsetf
   20. cfsetsnfsetf1
   21. cfsetsnfsetfo
   22. cfsetsnfsetf1o
   23. fsetprcnexALT
   24. fcoreslem1
   25. fcoreslem2
   26. fcoreslem3
   27. fcoreslem4
   28. fcores
   29. fcoresf1lem
   30. fcoresf1
   31. fcoresf1b
   32. fcoresfo
   33. fcoresfob
   34. fcoresf1ob
   35. f1cof1blem
   36. f1cof1b
   37. funfocofob
   38. fnfocofob
   39. focofob
   40. f1ocof1ob
   41. f1ocof1ob2