Metamath Proof Explorer


Table of Contents - 2.1.3. Class form not-free predicate

  1. wnfc
  2. nfcjust
  3. df-nfc
  4. nfci
  5. nfcii
  6. nfcr
  7. nfcrALT
  8. nfcri
  9. nfcd
  10. nfcrd
  11. nfcriOLD
  12. nfcriOLDOLD
  13. nfcrii
  14. nfcriiOLD
  15. nfcriOLDOLDOLD
  16. nfceqdf
  17. nfceqi
  18. nfcxfr
  19. nfcxfrd
  20. nfcv
  21. nfcvd
  22. nfab1
  23. nfnfc1
  24. clelsb3fw
  25. clelsb3f
  26. nfab
  27. nfabg
  28. nfaba1
  29. nfaba1g
  30. nfeqd
  31. nfeld
  32. nfnfc
  33. nfeq
  34. nfel
  35. nfeq1
  36. nfel1
  37. nfeq2
  38. nfel2
  39. drnfc1
  40. drnfc2
  41. nfabdw
  42. nfabd
  43. nfabd2
  44. dvelimdc
  45. dvelimc
  46. nfcvf
  47. nfcvf2
  48. cleqf
  49. abid2f
  50. abeq2f
  51. sbabel