Theorem ax-12 1340

Description: Rederive the original version of the axiom from ax-i12 1336. (Contributed by Mario Carneiro, 3-Feb-2015.)

Assertion

Ref	Expression
ax-12	⊢ (¬ ∀z z = x → (¬ ∀z z = y → (x = y → ∀z x = y)))

Proof of Theorem ax-12

Step	Hyp	Ref	Expression
1		ax-i12 1336	. . . 4 ⊢ (∀z z = x ∨ (∀z z = y ∨ ∀z(x = y → ∀z x = y)))
2	1	ori 621	. . 3 ⊢ (¬ ∀z z = x → (∀z z = y ∨ ∀z(x = y → ∀z x = y)))
3	2	ord 622	. 2 ⊢ (¬ ∀z z = x → (¬ ∀z z = y → ∀z(x = y → ∀z x = y)))
4		ax-4 1338	. 2 ⊢ (∀z(x = y → ∀z x = y) → (x = y → ∀z x = y))
5	3, 4	syl6 27	1 ⊢ (¬ ∀z z = x → (¬ ∀z z = y → (x = y → ∀z x = y)))

Syntax hints:  ¬ wn 3   → wi 4   ∨ wo 609  ∀wal 1271   = wceq 1329

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 97  ax-ia2 98  ax-ia3 99  ax-in2 528  ax-io 610  ax-i12 1336  ax-4 1338

This theorem depends on definitions:  df-bi 108