This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 (x = y \to \forall x φ) \to φ$

Proof

Step	Hyp	Ref	Expression
1		ax6v	$⊢ \neg \forall x \neg x = y$
2		con3	$⊢ (x = y \to \forall x φ) \to (\neg \forall x φ \to \neg x = y)$
3	2	al2imi	$⊢ \forall x (x = y \to \forall x φ) \to (\forall x \neg \forall x φ \to \forall x \neg x = y)$
4	1 3	mtoi	$⊢ \forall x (x = y \to \forall x φ) \to \neg \forall x \neg \forall x φ$
5		axc7	$⊢ \neg \forall x \neg \forall x φ \to φ$
6	4 5	syl	$⊢ \forall x (x = y \to \forall x φ) \to φ$