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. nfcrii
  12. nfceqdf
  13. nfceqi
  14. nfcxfr
  15. nfcxfrd
  16. nfcv
  17. nfcvd
  18. nfab1
  19. nfnfc1
  20. clelsb1fw
  21. clelsb1f
  22. nfab
  23. nfabg
  24. nfaba1
  25. nfaba1OLD
  26. nfaba1g
  27. nfeqd
  28. nfeld
  29. nfnfc
  30. nfeq
  31. nfel
  32. nfeq1
  33. nfel1
  34. nfeq2
  35. nfel2
  36. drnfc1
  37. drnfc2
  38. nfabdw
  39. nfabd
  40. nfabd2
  41. dvelimdc
  42. dvelimc
  43. nfcvf
  44. nfcvf2
  45. cleqf
  46. eqabf
  47. abid2f
  48. abid2fOLD
  49. sbabel