Theorem hbae-o

Description: All variables are effectively bound in an identical variable specifier. Version of hbae using ax-c11 . (Contributed by NM, 13-May-1993) (Proof modification is discouraged.) (New usage is discouraged.)

	Ref	Expression
Assertion	hbae-o	⊢ ( ∀ 𝑥 𝑥 = 𝑦 → ∀ 𝑧 ∀ 𝑥 𝑥 = 𝑦 )

Proof

Step	Hyp	Ref	Expression
1		ax-c5	⊢ ( ∀ 𝑥 𝑥 = 𝑦 → 𝑥 = 𝑦 )
2		ax-c9	⊢ ( ¬ ∀ 𝑧 𝑧 = 𝑥 → ( ¬ ∀ 𝑧 𝑧 = 𝑦 → ( 𝑥 = 𝑦 → ∀ 𝑧 𝑥 = 𝑦 ) ) )
3	1 2	syl7	⊢ ( ¬ ∀ 𝑧 𝑧 = 𝑥 → ( ¬ ∀ 𝑧 𝑧 = 𝑦 → ( ∀ 𝑥 𝑥 = 𝑦 → ∀ 𝑧 𝑥 = 𝑦 ) ) )
4		ax-c11	⊢ ( ∀ 𝑥 𝑥 = 𝑧 → ( ∀ 𝑥 𝑥 = 𝑦 → ∀ 𝑧 𝑥 = 𝑦 ) )
5	4	aecoms-o	⊢ ( ∀ 𝑧 𝑧 = 𝑥 → ( ∀ 𝑥 𝑥 = 𝑦 → ∀ 𝑧 𝑥 = 𝑦 ) )
6		ax-c11	⊢ ( ∀ 𝑥 𝑥 = 𝑦 → ( ∀ 𝑥 𝑥 = 𝑦 → ∀ 𝑦 𝑥 = 𝑦 ) )
7	6	pm2.43i	⊢ ( ∀ 𝑥 𝑥 = 𝑦 → ∀ 𝑦 𝑥 = 𝑦 )
8		ax-c11	⊢ ( ∀ 𝑦 𝑦 = 𝑧 → ( ∀ 𝑦 𝑥 = 𝑦 → ∀ 𝑧 𝑥 = 𝑦 ) )
9	7 8	syl5	⊢ ( ∀ 𝑦 𝑦 = 𝑧 → ( ∀ 𝑥 𝑥 = 𝑦 → ∀ 𝑧 𝑥 = 𝑦 ) )
10	9	aecoms-o	⊢ ( ∀ 𝑧 𝑧 = 𝑦 → ( ∀ 𝑥 𝑥 = 𝑦 → ∀ 𝑧 𝑥 = 𝑦 ) )
11	3 5 10	pm2.61ii	⊢ ( ∀ 𝑥 𝑥 = 𝑦 → ∀ 𝑧 𝑥 = 𝑦 )
12	11	axc4i-o	⊢ ( ∀ 𝑥 𝑥 = 𝑦 → ∀ 𝑥 ∀ 𝑧 𝑥 = 𝑦 )
13		ax-11	⊢ ( ∀ 𝑥 ∀ 𝑧 𝑥 = 𝑦 → ∀ 𝑧 ∀ 𝑥 𝑥 = 𝑦 )
14	12 13	syl	⊢ ( ∀ 𝑥 𝑥 = 𝑦 → ∀ 𝑧 ∀ 𝑥 𝑥 = 𝑦 )