Theorem ax-12 1393

Description: Rederive the original version of the axiom from ax-i12 1391. Note that we need ax-4 1392 for the derivation, but the proof of ax4 1423 is nontheless non-circular since it does not use ax-12. (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 1391	. . . 4 ⊢ (∀z z = x ∨ (∀z z = y ∨ ∀z(x = y → ∀z x = y)))
2	1	ori 618	. . 3 ⊢ (¬ ∀z z = x → (∀z z = y ∨ ∀z(x = y → ∀z x = y)))
3	2	ord 619	. 2 ⊢ (¬ ∀z z = x → (¬ ∀z z = y → ∀z(x = y → ∀z x = y)))
4		ax-4 1392	. 2 ⊢ (∀z(x = y → ∀z x = y) → (x = y → ∀z x = y))
5	3, 4	syl6 28	1 ⊢ (¬ ∀z z = x → (¬ ∀z z = y → (x = y → ∀z x = y)))

Syntax hints:  ¬ wn 3   → wi 4   ∨ wo 606  ∀wal 1335   = wceq 1383

This theorem is referenced by:  hbequidOLD  1398  a9wa9lem8  1413  a9wa9lem8OLD  1414  equidALT  1560  dvelimfALT  1585  ax17eq  1645  hbsb4  1686  sbcom  1696  dvelimALT  1800  ax11eq  1810  ax11indalem  1815  a12stdy4  1822  a12lem1  1823

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 8  ax-ia1 98  ax-ia2 99  ax-ia3 100  ax-in2 528  ax-io 607  ax-i12 1391  ax-4 1392

This theorem depends on definitions:  df-bi 109