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
|- ( A. x ( x = y -> A. x ph ) -> ph )

Detailed syntax breakdown

Step Hyp Ref Expression
0 vx
 |-  x
1 0 cv
 |-  x
2 vy
 |-  y
3 2 cv
 |-  y
4 1 3 wceq
 |-  x = y
5 wph
 |-  ph
6 5 0 wal
 |-  A. x ph
7 4 6 wi
 |-  ( x = y -> A. x ph )
8 7 0 wal
 |-  A. x ( x = y -> A. x ph )
9 8 5 wi
 |-  ( A. x ( x = y -> A. x ph ) -> ph )