Theorem bj-axc10

Description: Alternate proof of axc10 . Shorter. One can prove a version with DV ( x , y ) without ax-13 , by using ax6ev instead of ax6e . (Contributed by BJ, 31-Mar-2021) (Proof modification is discouraged.)

	Ref	Expression
Assertion	bj-axc10	⊢ ( ∀ 𝑥 ( 𝑥 = 𝑦 → ∀ 𝑥 𝜑 ) → 𝜑 )

Proof

Step	Hyp	Ref	Expression
1		ax6e	⊢ ∃ 𝑥 𝑥 = 𝑦
2		exim	⊢ ( ∀ 𝑥 ( 𝑥 = 𝑦 → ∀ 𝑥 𝜑 ) → ( ∃ 𝑥 𝑥 = 𝑦 → ∃ 𝑥 ∀ 𝑥 𝜑 ) )
3	1 2	mpi	⊢ ( ∀ 𝑥 ( 𝑥 = 𝑦 → ∀ 𝑥 𝜑 ) → ∃ 𝑥 ∀ 𝑥 𝜑 )
4		axc7e	⊢ ( ∃ 𝑥 ∀ 𝑥 𝜑 → 𝜑 )
5	3 4	syl	⊢ ( ∀ 𝑥 ( 𝑥 = 𝑦 → ∀ 𝑥 𝜑 ) → 𝜑 )