# 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 ${⊢}\forall {x}\phantom{\rule{.4em}{0ex}}\left({x}={y}\to \forall {x}\phantom{\rule{.4em}{0ex}}{\phi }\right)\to {\phi }$

### 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}{\phi }$
6 5 0 wal ${wff}\forall {x}\phantom{\rule{.4em}{0ex}}{\phi }$
7 4 6 wi ${wff}\left({x}={y}\to \forall {x}\phantom{\rule{.4em}{0ex}}{\phi }\right)$
8 7 0 wal ${wff}\forall {x}\phantom{\rule{.4em}{0ex}}\left({x}={y}\to \forall {x}\phantom{\rule{.4em}{0ex}}{\phi }\right)$
9 8 5 wi ${wff}\left(\forall {x}\phantom{\rule{.4em}{0ex}}\left({x}={y}\to \forall {x}\phantom{\rule{.4em}{0ex}}{\phi }\right)\to {\phi }\right)$