Theorem hbae 1740

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 1530	. . . 4 ⊢ (∀𝑧 𝑧 = 𝑥 ∨ (∀𝑧 𝑧 = 𝑦 ∨ ∀𝑧(𝑥 = 𝑦 → ∀𝑧 𝑥 = 𝑦)))
2		ax10o 1737	. . . . . 6 ⊢ (∀𝑥 𝑥 = 𝑧 → (∀𝑥 𝑥 = 𝑦 → ∀𝑧 𝑥 = 𝑦))
3	2	alequcoms 1538	. . . . 5 ⊢ (∀𝑧 𝑧 = 𝑥 → (∀𝑥 𝑥 = 𝑦 → ∀𝑧 𝑥 = 𝑦))
4		ax10o 1737	. . . . . . . . 9 ⊢ (∀𝑥 𝑥 = 𝑦 → (∀𝑥 𝑥 = 𝑦 → ∀𝑦 𝑥 = 𝑦))
5	4	pm2.43i 49	. . . . . . . 8 ⊢ (∀𝑥 𝑥 = 𝑦 → ∀𝑦 𝑥 = 𝑦)
6		ax10o 1737	. . . . . . . 8 ⊢ (∀𝑦 𝑦 = 𝑧 → (∀𝑦 𝑥 = 𝑦 → ∀𝑧 𝑥 = 𝑦))
7	5, 6	syl5 32	. . . . . . 7 ⊢ (∀𝑦 𝑦 = 𝑧 → (∀𝑥 𝑥 = 𝑦 → ∀𝑧 𝑥 = 𝑦))
8	7	alequcoms 1538	. . . . . 6 ⊢ (∀𝑧 𝑧 = 𝑦 → (∀𝑥 𝑥 = 𝑦 → ∀𝑧 𝑥 = 𝑦))
9		ax-4 1532	. . . . . . . 8 ⊢ (∀𝑥 𝑥 = 𝑦 → 𝑥 = 𝑦)
10	9	imim1i 60	. . . . . . 7 ⊢ ((𝑥 = 𝑦 → ∀𝑧 𝑥 = 𝑦) → (∀𝑥 𝑥 = 𝑦 → ∀𝑧 𝑥 = 𝑦))
11	10	sps 1559	. . . . . 6 ⊢ (∀𝑧(𝑥 = 𝑦 → ∀𝑧 𝑥 = 𝑦) → (∀𝑥 𝑥 = 𝑦 → ∀𝑧 𝑥 = 𝑦))
12	8, 11	jaoi 717	. . . . 5 ⊢ ((∀𝑧 𝑧 = 𝑦 ∨ ∀𝑧(𝑥 = 𝑦 → ∀𝑧 𝑥 = 𝑦)) → (∀𝑥 𝑥 = 𝑦 → ∀𝑧 𝑥 = 𝑦))
13	3, 12	jaoi 717	. . . 4 ⊢ ((∀𝑧 𝑧 = 𝑥 ∨ (∀𝑧 𝑧 = 𝑦 ∨ ∀𝑧(𝑥 = 𝑦 → ∀𝑧 𝑥 = 𝑦))) → (∀𝑥 𝑥 = 𝑦 → ∀𝑧 𝑥 = 𝑦))
14	1, 13	ax-mp 5	. . 3 ⊢ (∀𝑥 𝑥 = 𝑦 → ∀𝑧 𝑥 = 𝑦)
15	14	a5i 1565	. 2 ⊢ (∀𝑥 𝑥 = 𝑦 → ∀𝑥∀𝑧 𝑥 = 𝑦)
16		ax-7 1470	. 2 ⊢ (∀𝑥∀𝑧 𝑥 = 𝑦 → ∀𝑧∀𝑥 𝑥 = 𝑦)
17	15, 16	syl 14	1 ⊢ (∀𝑥 𝑥 = 𝑦 → ∀𝑧∀𝑥 𝑥 = 𝑦)

Syntax hints:   → wi 4   ∨ wo 709  ∀wal 1370   = wceq 1372

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-io 710  ax-5 1469  ax-7 1470  ax-gen 1471  ax-ie2 1516  ax-8 1526  ax-10 1527  ax-11 1528  ax-i12 1529  ax-4 1532  ax-17 1548  ax-i9 1552  ax-ial 1556

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  nfae  1741  hbaes  1742  hbnae  1743  dral1  1752  dral2  1753  drex2  1754  drex1  1820  aev  1834  sbcomxyyz  1999  exists1  2149