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. nfceqdfOLD
  18. nfceqi
  19. nfcxfr
  20. nfcxfrd
  21. nfcv
  22. nfcvd
  23. nfab1
  24. nfnfc1
  25. clelsb1fw
  26. clelsb1f
  27. nfab
  28. nfabg
  29. nfaba1
  30. nfaba1g
  31. nfeqd
  32. nfeld
  33. nfnfc
  34. nfeq
  35. nfel
  36. nfeq1
  37. nfel1
  38. nfeq2
  39. nfel2
  40. drnfc1
  41. drnfc1OLD
  42. drnfc2
  43. drnfc2OLD
  44. nfabdw
  45. nfabdwOLD
  46. nfabd
  47. nfabd2
  48. dvelimdc
  49. dvelimc
  50. nfcvf
  51. nfcvf2
  52. cleqf
  53. abid2f
  54. abeq2f
  55. sbabel
  56. sbabelOLD