Metamath Proof Explorer


Axiom ax-c10

Description: A variant of ax6 . Axiom scheme C10' 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 axc10 . (Contributed by NM, 10-Jan-1993) (New usage is discouraged.)

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

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 wph wff φ
6 5 0 wal wff x φ
7 4 6 wi wff x = y x φ
8 7 0 wal wff x x = y x φ
9 8 5 wi wff x x = y x φ φ