Metamath Proof Explorer
Table of Contents - 20.16.6.2. Identity relation (complements)
Complements on the identity relation.
- bj-opabssvv
- bj-funidres
- bj-opelidb
- bj-opelidb1
- bj-inexeqex
- bj-elsn0
- bj-opelid
- bj-ideqg
- bj-ideqgALT
- bj-ideqb
- bj-idres
- bj-opelidres
- bj-idreseq
- bj-idreseqb
- bj-ideqg1
- bj-ideqg1ALT
- bj-opelidb1ALT
- bj-elid3
- bj-elid4
- bj-elid5
- bj-elid6
- bj-elid7