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	⊢ ( ∀ 𝑥 ( 𝑥 = 𝑦 → ∀ 𝑥 𝜑 ) → 𝜑 )

Proof

Step	Hyp	Ref	Expression
1		ax6v	⊢ ¬ ∀ 𝑥 ¬ 𝑥 = 𝑦
2		con3	⊢ ( ( 𝑥 = 𝑦 → ∀ 𝑥 𝜑 ) → ( ¬ ∀ 𝑥 𝜑 → ¬ 𝑥 = 𝑦 ) )
3	2	al2imi	⊢ ( ∀ 𝑥 ( 𝑥 = 𝑦 → ∀ 𝑥 𝜑 ) → ( ∀ 𝑥 ¬ ∀ 𝑥 𝜑 → ∀ 𝑥 ¬ 𝑥 = 𝑦 ) )
4	1 3	mtoi	⊢ ( ∀ 𝑥 ( 𝑥 = 𝑦 → ∀ 𝑥 𝜑 ) → ¬ ∀ 𝑥 ¬ ∀ 𝑥 𝜑 )
5		axc7	⊢ ( ¬ ∀ 𝑥 ¬ ∀ 𝑥 𝜑 → 𝜑 )
6	4 5	syl	⊢ ( ∀ 𝑥 ( 𝑥 = 𝑦 → ∀ 𝑥 𝜑 ) → 𝜑 )