Theorem hbae 1706

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 1496	. . . 4 ⊢ (∀𝑧 𝑧 = 𝑥 ∨ (∀𝑧 𝑧 = 𝑦 ∨ ∀𝑧(𝑥 = 𝑦 → ∀𝑧 𝑥 = 𝑦)))
2		ax10o 1703	. . . . . 6 ⊢ (∀𝑥 𝑥 = 𝑧 → (∀𝑥 𝑥 = 𝑦 → ∀𝑧 𝑥 = 𝑦))
3	2	alequcoms 1504	. . . . 5 ⊢ (∀𝑧 𝑧 = 𝑥 → (∀𝑥 𝑥 = 𝑦 → ∀𝑧 𝑥 = 𝑦))
4		ax10o 1703	. . . . . . . . 9 ⊢ (∀𝑥 𝑥 = 𝑦 → (∀𝑥 𝑥 = 𝑦 → ∀𝑦 𝑥 = 𝑦))
5	4	pm2.43i 49	. . . . . . . 8 ⊢ (∀𝑥 𝑥 = 𝑦 → ∀𝑦 𝑥 = 𝑦)
6		ax10o 1703	. . . . . . . 8 ⊢ (∀𝑦 𝑦 = 𝑧 → (∀𝑦 𝑥 = 𝑦 → ∀𝑧 𝑥 = 𝑦))
7	5, 6	syl5 32	. . . . . . 7 ⊢ (∀𝑦 𝑦 = 𝑧 → (∀𝑥 𝑥 = 𝑦 → ∀𝑧 𝑥 = 𝑦))
8	7	alequcoms 1504	. . . . . 6 ⊢ (∀𝑧 𝑧 = 𝑦 → (∀𝑥 𝑥 = 𝑦 → ∀𝑧 𝑥 = 𝑦))
9		ax-4 1498	. . . . . . . 8 ⊢ (∀𝑥 𝑥 = 𝑦 → 𝑥 = 𝑦)
10	9	imim1i 60	. . . . . . 7 ⊢ ((𝑥 = 𝑦 → ∀𝑧 𝑥 = 𝑦) → (∀𝑥 𝑥 = 𝑦 → ∀𝑧 𝑥 = 𝑦))
11	10	sps 1525	. . . . . 6 ⊢ (∀𝑧(𝑥 = 𝑦 → ∀𝑧 𝑥 = 𝑦) → (∀𝑥 𝑥 = 𝑦 → ∀𝑧 𝑥 = 𝑦))
12	8, 11	jaoi 706	. . . . 5 ⊢ ((∀𝑧 𝑧 = 𝑦 ∨ ∀𝑧(𝑥 = 𝑦 → ∀𝑧 𝑥 = 𝑦)) → (∀𝑥 𝑥 = 𝑦 → ∀𝑧 𝑥 = 𝑦))
13	3, 12	jaoi 706	. . . 4 ⊢ ((∀𝑧 𝑧 = 𝑥 ∨ (∀𝑧 𝑧 = 𝑦 ∨ ∀𝑧(𝑥 = 𝑦 → ∀𝑧 𝑥 = 𝑦))) → (∀𝑥 𝑥 = 𝑦 → ∀𝑧 𝑥 = 𝑦))
14	1, 13	ax-mp 5	. . 3 ⊢ (∀𝑥 𝑥 = 𝑦 → ∀𝑧 𝑥 = 𝑦)
15	14	a5i 1531	. 2 ⊢ (∀𝑥 𝑥 = 𝑦 → ∀𝑥∀𝑧 𝑥 = 𝑦)
16		ax-7 1436	. 2 ⊢ (∀𝑥∀𝑧 𝑥 = 𝑦 → ∀𝑧∀𝑥 𝑥 = 𝑦)
17	15, 16	syl 14	1 ⊢ (∀𝑥 𝑥 = 𝑦 → ∀𝑧∀𝑥 𝑥 = 𝑦)

Syntax hints:   → wi 4   ∨ wo 698  ∀wal 1341   = wceq 1343

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-io 699  ax-5 1435  ax-7 1436  ax-gen 1437  ax-ie2 1482  ax-8 1492  ax-10 1493  ax-11 1494  ax-i12 1495  ax-4 1498  ax-17 1514  ax-i9 1518  ax-ial 1522

This theorem depends on definitions:  df-bi 116

This theorem is referenced by:  nfae  1707  hbaes  1708  hbnae  1709  dral1  1718  dral2  1719  drex2  1720  drex1  1786  aev  1800  sbcomxyyz  1960  exists1  2110