Metamath Proof Explorer

Table of Contents - 21.18.5.5. Lemmas for class substitution

Some useful theorems for dealing with substitutions: sbbi, sbcbig, sbcel1g, sbcel2, sbcel12, sbceqg, csbvarg.

1. bj-sbeqALT
2. bj-sbeq
3. bj-sbceqgALT
4. bj-csbsnlem
5. bj-csbsn
6. bj-sbel1
7. bj-abv
8. bj-abvALT
9. bj-ab0
10. bj-abf
11. bj-csbprc