Theorem hbae 1603

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 1400	. . . 4 ⊢ (∀z z = x ∨ (∀z z = y ∨ ∀z(x = y → ∀z x = y)))
2		ax10o 1600	. . . . . 6 ⊢ (∀x x = z → (∀x x = y → ∀z x = y))
3	2	alequcoms 1406	. . . . 5 ⊢ (∀z z = x → (∀x x = y → ∀z x = y))
4		ax10o 1600	. . . . . . . . 9 ⊢ (∀x x = y → (∀x x = y → ∀y x = y))
5	4	pm2.43i 43	. . . . . . . 8 ⊢ (∀x x = y → ∀y x = y)
6		ax10o 1600	. . . . . . . 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 1406	. . . . . 6 ⊢ (∀z z = y → (∀x x = y → ∀z x = y))
9		ax-4 1397	. . . . . . . 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 1427	. . . . . 6 ⊢ (∀z(x = y → ∀z x = y) → (∀x x = y → ∀z x = y))
12	8, 11	jaoi 635	. . . . 5 ⊢ ((∀z z = y ∨ ∀z(x = y → ∀z x = y)) → (∀x x = y → ∀z x = y))
13	3, 12	jaoi 635	. . . 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 1432	. 2 ⊢ (∀x x = y → ∀x∀z x = y)
16		ax-7 1334	. 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 628  ∀wal 1240   = wceq 1242

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 629  ax-5 1333  ax-7 1334  ax-gen 1335  ax-ie2 1380  ax-8 1392  ax-10 1393  ax-11 1394  ax-i12 1395  ax-4 1397  ax-17 1416  ax-i9 1420  ax-ial 1424

This theorem depends on definitions:  df-bi 110

This theorem is referenced by:  nfae  1604  hbaes  1605  hbnae  1606  dral1  1615  dral2  1616  drex2  1617  drex1  1676  aev  1690  sbcomxyyz  1843  exists1  1993