Metamath Proof Explorer


Table of Contents - 20.16.6.2. Identity relation (complements)

Complements on the identity relation.

  1. bj-opabssvv
  2. bj-funidres
  3. bj-opelidb
  4. bj-opelidb1
  5. bj-inexeqex
  6. bj-elsn0
  7. bj-opelid
  8. bj-ideqg
  9. bj-ideqgALT
  10. bj-ideqb
  11. bj-idres
  12. bj-opelidres
  13. bj-idreseq
  14. bj-idreseqb
  15. bj-ideqg1
  16. bj-ideqg1ALT
  17. bj-opelidb1ALT
  18. bj-elid3
  19. bj-elid4
  20. bj-elid5
  21. bj-elid6
  22. bj-elid7