Theorem hbae 1588

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	⊢ (∀x x = y → ∀z∀x x = y)

Proof of Theorem hbae

Step	Hyp	Ref	Expression
1		ax12or 1384	. . . 4 ⊢ (∀z z = x ∨ (∀z z = y ∨ ∀z(x = y → ∀z x = y)))
2		ax10o 1585	. . . . . 6 ⊢ (∀x x = z → (∀x x = y → ∀z x = y))
3	2	alequcoms 1390	. . . . 5 ⊢ (∀z z = x → (∀x x = y → ∀z x = y))
4		ax10o 1585	. . . . . . . . 9 ⊢ (∀x x = y → (∀x x = y → ∀y x = y))
5	4	pm2.43i 43	. . . . . . . 8 ⊢ (∀x x = y → ∀y x = y)
6		ax10o 1585	. . . . . . . 8 ⊢ (∀y y = z → (∀y x = y → ∀z x = y))
7	5, 6	syl5 28	. . . . . . 7 ⊢ (∀y y = z → (∀x x = y → ∀z x = y))
8	7	alequcoms 1390	. . . . . 6 ⊢ (∀z z = y → (∀x x = y → ∀z x = y))
9		ax-4 1381	. . . . . . . 8 ⊢ (∀x x = y → x = y)
10	9	imim1i 54	. . . . . . 7 ⊢ ((x = y → ∀z x = y) → (∀x x = y → ∀z x = y))
11	10	sps 1412	. . . . . 6 ⊢ (∀z(x = y → ∀z x = y) → (∀x x = y → ∀z x = y))
12	8, 11	jaoi 623	. . . . 5 ⊢ ((∀z z = y ∨ ∀z(x = y → ∀z x = y)) → (∀x x = y → ∀z x = y))
13	3, 12	jaoi 623	. . . 4 ⊢ ((∀z z = x ∨ (∀z z = y ∨ ∀z(x = y → ∀z x = y))) → (∀x x = y → ∀z x = y))
14	1, 13	ax-mp 7	. . 3 ⊢ (∀x x = y → ∀z x = y)
15	14	a5i 1417	. 2 ⊢ (∀x x = y → ∀x∀z x = y)
16		ax-7 1317	. 2 ⊢ (∀x∀z x = y → ∀z∀x x = y)
17	15, 16	syl 14	1 ⊢ (∀x x = y → ∀z∀x x = y)

Syntax hints:   → wi 4   ∨ wo 616  ∀wal 1226   = wceq 1228

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100  ax-ia3 101  ax-io 617  ax-5 1316  ax-7 1317  ax-gen 1318  ax-ie2 1364  ax-8 1376  ax-10 1377  ax-11 1378  ax-i12 1379  ax-4 1381  ax-17 1400  ax-i9 1404  ax-ial 1409

This theorem depends on definitions:  df-bi 110

This theorem is referenced by:  nfae  1589  hbaes  1590  hbnae  1591  dral1  1600  dral2  1601  drex2  1602  drex1  1661  aev  1675  sbcomxyyz  1828  exists1  1978