Metamath Proof Explorer


Table of Contents - 20.33.3.5. _Begriffsschrift_ Chapter II with logical equivalence

Here we leverage df-ifp to partition a wff into two that are disjoint with the selector wff.

Thus if we are given then we replace the concept (illegal in our notation ) with to reason about the values of the "function." Likewise, we replace the similarly illegal concept with .

  1. axfrege52a
  2. ax-frege52a
  3. frege52aid
  4. frege53aid
  5. frege53a
  6. axfrege54a
  7. ax-frege54a
  8. frege54cor0a
  9. frege54cor1a
  10. frege55aid
  11. frege55lem1a
  12. frege55lem2a
  13. frege55a
  14. frege55cor1a
  15. frege56aid
  16. frege56a
  17. frege57aid
  18. frege57a
  19. axfrege58a
  20. ax-frege58a
  21. frege58acor
  22. frege59a
  23. frege60a
  24. frege61a
  25. frege62a
  26. frege63a
  27. frege64a
  28. frege65a
  29. frege66a
  30. frege67a
  31. frege68a