# Metamath Proof Explorer

## Theorem ax12indn

Description: Induction step for constructing a substitution instance of ax-c15 without using ax-c15 . Negation case. (Contributed by NM, 21-Jan-2007) (Proof modification is discouraged.) (New usage is discouraged.)

Ref Expression
Hypothesis ax12indn.1 ${⊢}¬\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)$
Assertion ax12indn ${⊢}¬\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 ax12indn.1 ${⊢}¬\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)$
2 19.8a ${⊢}\left({x}={y}\wedge ¬{\phi }\right)\to \exists {x}\phantom{\rule{.4em}{0ex}}\left({x}={y}\wedge ¬{\phi }\right)$
3 exanali ${⊢}\exists {x}\phantom{\rule{.4em}{0ex}}\left({x}={y}\wedge ¬{\phi }\right)↔¬\forall {x}\phantom{\rule{.4em}{0ex}}\left({x}={y}\to {\phi }\right)$
4 hbn1 ${⊢}¬\forall {x}\phantom{\rule{.4em}{0ex}}{x}={y}\to \forall {x}\phantom{\rule{.4em}{0ex}}¬\forall {x}\phantom{\rule{.4em}{0ex}}{x}={y}$
5 hbn1 ${⊢}¬\forall {x}\phantom{\rule{.4em}{0ex}}\left({x}={y}\to {\phi }\right)\to \forall {x}\phantom{\rule{.4em}{0ex}}¬\forall {x}\phantom{\rule{.4em}{0ex}}\left({x}={y}\to {\phi }\right)$
6 con3 ${⊢}\left({\phi }\to \forall {x}\phantom{\rule{.4em}{0ex}}\left({x}={y}\to {\phi }\right)\right)\to \left(¬\forall {x}\phantom{\rule{.4em}{0ex}}\left({x}={y}\to {\phi }\right)\to ¬{\phi }\right)$
7 1 6 syl6 ${⊢}¬\forall {x}\phantom{\rule{.4em}{0ex}}{x}={y}\to \left({x}={y}\to \left(¬\forall {x}\phantom{\rule{.4em}{0ex}}\left({x}={y}\to {\phi }\right)\to ¬{\phi }\right)\right)$
8 7 com23 ${⊢}¬\forall {x}\phantom{\rule{.4em}{0ex}}{x}={y}\to \left(¬\forall {x}\phantom{\rule{.4em}{0ex}}\left({x}={y}\to {\phi }\right)\to \left({x}={y}\to ¬{\phi }\right)\right)$
9 4 5 8 alrimdh ${⊢}¬\forall {x}\phantom{\rule{.4em}{0ex}}{x}={y}\to \left(¬\forall {x}\phantom{\rule{.4em}{0ex}}\left({x}={y}\to {\phi }\right)\to \forall {x}\phantom{\rule{.4em}{0ex}}\left({x}={y}\to ¬{\phi }\right)\right)$
10 3 9 syl5bi ${⊢}¬\forall {x}\phantom{\rule{.4em}{0ex}}{x}={y}\to \left(\exists {x}\phantom{\rule{.4em}{0ex}}\left({x}={y}\wedge ¬{\phi }\right)\to \forall {x}\phantom{\rule{.4em}{0ex}}\left({x}={y}\to ¬{\phi }\right)\right)$
11 2 10 syl5 ${⊢}¬\forall {x}\phantom{\rule{.4em}{0ex}}{x}={y}\to \left(\left({x}={y}\wedge ¬{\phi }\right)\to \forall {x}\phantom{\rule{.4em}{0ex}}\left({x}={y}\to ¬{\phi }\right)\right)$
12 11 expd ${⊢}¬\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)$