# Metamath Proof Explorer

## Theorem bj-axc10v

Description: Version of axc10 with a disjoint variable condition, which does not require ax-13 . (Contributed by BJ, 14-Jun-2019) (Proof modification is discouraged.)

Ref Expression
Assertion bj-axc10v ${⊢}\forall {x}\phantom{\rule{.4em}{0ex}}\left({x}={y}\to \forall {x}\phantom{\rule{.4em}{0ex}}{\phi }\right)\to {\phi }$

### Proof

Step Hyp Ref Expression
1 ax6v ${⊢}¬\forall {x}\phantom{\rule{.4em}{0ex}}¬{x}={y}$
2 con3 ${⊢}\left({x}={y}\to \forall {x}\phantom{\rule{.4em}{0ex}}{\phi }\right)\to \left(¬\forall {x}\phantom{\rule{.4em}{0ex}}{\phi }\to ¬{x}={y}\right)$
3 2 al2imi ${⊢}\forall {x}\phantom{\rule{.4em}{0ex}}\left({x}={y}\to \forall {x}\phantom{\rule{.4em}{0ex}}{\phi }\right)\to \left(\forall {x}\phantom{\rule{.4em}{0ex}}¬\forall {x}\phantom{\rule{.4em}{0ex}}{\phi }\to \forall {x}\phantom{\rule{.4em}{0ex}}¬{x}={y}\right)$
4 1 3 mtoi ${⊢}\forall {x}\phantom{\rule{.4em}{0ex}}\left({x}={y}\to \forall {x}\phantom{\rule{.4em}{0ex}}{\phi }\right)\to ¬\forall {x}\phantom{\rule{.4em}{0ex}}¬\forall {x}\phantom{\rule{.4em}{0ex}}{\phi }$
5 axc7 ${⊢}¬\forall {x}\phantom{\rule{.4em}{0ex}}¬\forall {x}\phantom{\rule{.4em}{0ex}}{\phi }\to {\phi }$
6 4 5 syl ${⊢}\forall {x}\phantom{\rule{.4em}{0ex}}\left({x}={y}\to \forall {x}\phantom{\rule{.4em}{0ex}}{\phi }\right)\to {\phi }$