Metamath Proof Explorer


Axiom ax-c11

Description: Axiom ax-c11 was the original version of ax-c11n ("n" for "new"), before it was discovered (in May 2008) that the shorter ax-c11n could replace it. It appears as Axiom scheme C11' in Megill p. 448 (p. 16 of the preprint).

This axiom is obsolete and should no longer be used. It is proved above as Theorem axc11 . (Contributed by NM, 10-May-1993) (New usage is discouraged.)

Ref Expression
Assertion ax-c11 x x = y x φ y φ

Detailed syntax breakdown

Step Hyp Ref Expression
0 vx setvar x
1 0 cv setvar x
2 vy setvar y
3 2 cv setvar y
4 1 3 wceq wff x = y
5 4 0 wal wff x x = y
6 wph wff φ
7 6 0 wal wff x φ
8 6 2 wal wff y φ
9 7 8 wi wff x φ y φ
10 5 9 wi wff x x = y x φ y φ