# Metamath Proof Explorer

## Theorem ax12f

Description: Basis step for constructing a substitution instance of ax-c15 without using ax-c15 . We can start with any formula ph in which x is not free. (Contributed by NM, 21-Jan-2007) (Proof modification is discouraged.) (New usage is discouraged.)

Ref Expression
Hypothesis ax12f.1 ${⊢}{\phi }\to \forall {x}\phantom{\rule{.4em}{0ex}}{\phi }$
Assertion ax12f ${⊢}¬\forall {x}\phantom{\rule{.4em}{0ex}}{x}={y}\to \left({x}={y}\to \left({\phi }\to \forall {x}\phantom{\rule{.4em}{0ex}}\left({x}={y}\to {\phi }\right)\right)\right)$

### Proof

Step Hyp Ref Expression
1 ax12f.1 ${⊢}{\phi }\to \forall {x}\phantom{\rule{.4em}{0ex}}{\phi }$
2 ax-1 ${⊢}{\phi }\to \left({x}={y}\to {\phi }\right)$
3 1 2 alrimih ${⊢}{\phi }\to \forall {x}\phantom{\rule{.4em}{0ex}}\left({x}={y}\to {\phi }\right)$
4 3 2a1i ${⊢}¬\forall {x}\phantom{\rule{.4em}{0ex}}{x}={y}\to \left({x}={y}\to \left({\phi }\to \forall {x}\phantom{\rule{.4em}{0ex}}\left({x}={y}\to {\phi }\right)\right)\right)$