Theorem ax-12 1335

Description: Rederive the original version of the axiom from ax-i12 1331. (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 1331	. . . 4 ⊢ (∀z z = x ∨ (∀z z = y ∨ ∀z(x = y → ∀z x = y)))
2	1	ori 620	. . 3 ⊢ (¬ ∀z z = x → (∀z z = y ∨ ∀z(x = y → ∀z x = y)))
3	2	ord 621	. 2 ⊢ (¬ ∀z z = x → (¬ ∀z z = y → ∀z(x = y → ∀z x = y)))
4		ax-4 1333	. 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 608  ∀wal 1266   = wceq 1324

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 609  ax-i12 1331  ax-4 1333

This theorem depends on definitions:  df-bi 108