Metamath Proof Explorer


Table of Contents - 2.3.4. Ordered-pair class abstractions (cont.)

  1. opabidw
  2. opabid
  3. elopab
  4. rexopabb
  5. opelopabsbALT
  6. opelopabsb
  7. brabsb
  8. opelopabt
  9. opelopabga
  10. brabga
  11. opelopab2a
  12. opelopaba
  13. braba
  14. opelopabg
  15. brabg
  16. opelopabgf
  17. opelopab2
  18. opelopab
  19. brab
  20. opelopabaf
  21. opelopabf
  22. ssopab2
  23. ssopab2bw
  24. eqopab2bw
  25. ssopab2b
  26. ssopab2i
  27. ssopab2dv
  28. eqopab2b
  29. opabn0
  30. opab0
  31. csbopab
  32. csbopabgALT
  33. csbmpt12
  34. csbmpt2
  35. iunopab
  36. elopabr
  37. elopabran
  38. rbropapd
  39. rbropap
  40. 2rbropap
  41. 0nelopab
  42. brabv