Theorem hbae 1653

Description: All variables are effectively bound in an identical variable specifier. (Contributed by NM, 5-Aug-1993.) (Revised by NM, 3-Feb-2015.)

Assertion

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

Proof of Theorem hbae

Step	Hyp	Ref	Expression
1		ax12or 1448	. . . 4 ⊢ (∀𝑧 𝑧 = 𝑥 ∨ (∀𝑧 𝑧 = 𝑦 ∨ ∀𝑧(𝑥 = 𝑦 → ∀𝑧 𝑥 = 𝑦)))
2		ax10o 1650	. . . . . 6 ⊢ (∀𝑥 𝑥 = 𝑧 → (∀𝑥 𝑥 = 𝑦 → ∀𝑧 𝑥 = 𝑦))
3	2	alequcoms 1454	. . . . 5 ⊢ (∀𝑧 𝑧 = 𝑥 → (∀𝑥 𝑥 = 𝑦 → ∀𝑧 𝑥 = 𝑦))
4		ax10o 1650	. . . . . . . . 9 ⊢ (∀𝑥 𝑥 = 𝑦 → (∀𝑥 𝑥 = 𝑦 → ∀𝑦 𝑥 = 𝑦))
5	4	pm2.43i 48	. . . . . . . 8 ⊢ (∀𝑥 𝑥 = 𝑦 → ∀𝑦 𝑥 = 𝑦)
6		ax10o 1650	. . . . . . . 8 ⊢ (∀𝑦 𝑦 = 𝑧 → (∀𝑦 𝑥 = 𝑦 → ∀𝑧 𝑥 = 𝑦))
7	5, 6	syl5 32	. . . . . . 7 ⊢ (∀𝑦 𝑦 = 𝑧 → (∀𝑥 𝑥 = 𝑦 → ∀𝑧 𝑥 = 𝑦))
8	7	alequcoms 1454	. . . . . 6 ⊢ (∀𝑧 𝑧 = 𝑦 → (∀𝑥 𝑥 = 𝑦 → ∀𝑧 𝑥 = 𝑦))
9		ax-4 1445	. . . . . . . 8 ⊢ (∀𝑥 𝑥 = 𝑦 → 𝑥 = 𝑦)
10	9	imim1i 59	. . . . . . 7 ⊢ ((𝑥 = 𝑦 → ∀𝑧 𝑥 = 𝑦) → (∀𝑥 𝑥 = 𝑦 → ∀𝑧 𝑥 = 𝑦))
11	10	sps 1475	. . . . . 6 ⊢ (∀𝑧(𝑥 = 𝑦 → ∀𝑧 𝑥 = 𝑦) → (∀𝑥 𝑥 = 𝑦 → ∀𝑧 𝑥 = 𝑦))
12	8, 11	jaoi 671	. . . . 5 ⊢ ((∀𝑧 𝑧 = 𝑦 ∨ ∀𝑧(𝑥 = 𝑦 → ∀𝑧 𝑥 = 𝑦)) → (∀𝑥 𝑥 = 𝑦 → ∀𝑧 𝑥 = 𝑦))
13	3, 12	jaoi 671	. . . 4 ⊢ ((∀𝑧 𝑧 = 𝑥 ∨ (∀𝑧 𝑧 = 𝑦 ∨ ∀𝑧(𝑥 = 𝑦 → ∀𝑧 𝑥 = 𝑦))) → (∀𝑥 𝑥 = 𝑦 → ∀𝑧 𝑥 = 𝑦))
14	1, 13	ax-mp 7	. . 3 ⊢ (∀𝑥 𝑥 = 𝑦 → ∀𝑧 𝑥 = 𝑦)
15	14	a5i 1480	. 2 ⊢ (∀𝑥 𝑥 = 𝑦 → ∀𝑥∀𝑧 𝑥 = 𝑦)
16		ax-7 1382	. 2 ⊢ (∀𝑥∀𝑧 𝑥 = 𝑦 → ∀𝑧∀𝑥 𝑥 = 𝑦)
17	15, 16	syl 14	1 ⊢ (∀𝑥 𝑥 = 𝑦 → ∀𝑧∀𝑥 𝑥 = 𝑦)

Syntax hints:   → wi 4   ∨ wo 664  ∀wal 1287   = wceq 1289

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106  ax-io 665  ax-5 1381  ax-7 1382  ax-gen 1383  ax-ie2 1428  ax-8 1440  ax-10 1441  ax-11 1442  ax-i12 1443  ax-4 1445  ax-17 1464  ax-i9 1468  ax-ial 1472

This theorem depends on definitions:  df-bi 115

This theorem is referenced by:  nfae  1654  hbaes  1655  hbnae  1656  dral1  1665  dral2  1666  drex2  1667  drex1  1726  aev  1740  sbcomxyyz  1894  exists1  2044