Theorem hbae 1144

Description: All variables are effectively bound in an identical variable specifier.

Assertion

Ref	Expression
hbae	⊢ (∀x x = y → ∀z∀x x = y)

Proof of Theorem hbae

Step	Hyp	Ref	Expression
1		ax-12 967	. . . . 5 ⊢ (¬ ∀z z = x → (¬ ∀z z = y → (x = y → ∀z x = y)))
2		ax-4 972	. . . . 5 ⊢ (∀x x = y → x = y)
3	1, 2	syl7 23	. . . 4 ⊢ (¬ ∀z z = x → (¬ ∀z z = y → (∀x x = y → ∀z x = y)))
4		ax-10o 1139	. . . . 5 ⊢ (∀x x = z → (∀x x = y → ∀z x = y))
5	4	alequcoms 1142	. . . 4 ⊢ (∀z z = x → (∀x x = y → ∀z x = y))
6		ax-10o 1139	. . . . . 6 ⊢ (∀y y = z → (∀y x = y → ∀z x = y))
7		ax-10o 1139	. . . . . . 7 ⊢ (∀x x = y → (∀x x = y → ∀y x = y))
8	7	pm2.43i 64	. . . . . 6 ⊢ (∀x x = y → ∀y x = y)
9	6, 8	syl5 21	. . . . 5 ⊢ (∀y y = z → (∀x x = y → ∀z x = y))
10	9	alequcoms 1142	. . . 4 ⊢ (∀z z = y → (∀x x = y → ∀z x = y))
11	3, 5, 10	pm2.61ii 130	. . 3 ⊢ (∀x x = y → ∀z x = y)
12	11	a5i 988	. 2 ⊢ (∀x x = y → ∀x∀z x = y)
13		ax-7 961	. 2 ⊢ (∀x∀z x = y → ∀z∀x x = y)
14	12, 13	syl 10	1 ⊢ (∀x x = y → ∀z∀x x = y)

Syntax hints:  ¬ wn 2   → wi 3  ∀wal 953   = wceq 955

This theorem is referenced by:  hbaes 1145  hbnae 1146  dral1 1153  dral2 1154  drex2 1156  equvini 1167  sbequ5 1189  aev 1207  hbsb4 1247  sbcom 1257  a16g 1275  sbcom2 1333  a12stdy3 1373  exists1 1456  axextnd 4926  axrepnd 4929  axunndlem1 4930  axunnd 4931  axpowndlem3 4934  axpownd 4936  axregndlem1 4937  axregnd 4939  axacndlem1 4942  axacndlem2 4943  axacndlem3 4944  axacndlem4 4945  axacndlem5 4946  axacnd 4947

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 961  ax-gen 962  ax-10 965  ax-12 967  ax-4 972  ax-5o 974  ax-10o 1139

Copyright terms: Public domain