Metamath Proof Explorer

Table of Contents - 20.25.2. Obsolete schemes ax-c4,c5,c7,c10,c11,c11n,c15,c9,c14,c16

These older axiom schemes are obsolete and should not be used outside of this section. They are proved above as theorems axc4 , sp, axc7, axc10, axc11, axc11n, axc15, axc9, axc14, and axc16.

1. ax-c5
2. ax-c4
3. ax-c7
4. ax-c10
5. ax-c11
6. ax-c11n
7. ax-c15
8. ax-c9
9. ax-c14
10. ax-c16