Theorem ax-12 1399

Description: Rederive the original version of the axiom from ax-i12 1395. (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 1395	. . . 4 ⊢ (∀z z = x ∨ (∀z z = y ∨ ∀z(x = y → ∀z x = y)))
2	1	ori 641	. . 3 ⊢ (¬ ∀z z = x → (∀z z = y ∨ ∀z(x = y → ∀z x = y)))
3	2	ord 642	. 2 ⊢ (¬ ∀z z = x → (¬ ∀z z = y → ∀z(x = y → ∀z x = y)))
4		ax-4 1397	. 2 ⊢ (∀z(x = y → ∀z x = y) → (x = y → ∀z x = y))
5	3, 4	syl6 29	1 ⊢ (¬ ∀z z = x → (¬ ∀z z = y → (x = y → ∀z x = y)))

Syntax hints:  ¬ wn 3   → 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-in2 545  ax-io 629  ax-i12 1395  ax-4 1397

This theorem depends on definitions:  df-bi 110

This theorem is referenced by: (None)