Theorem ax-9 1418

Description: Derive ax-9 1418 from ax-i9 1417, the modified version for intuitionistic logic.

Assertion

Ref	Expression
ax-9	⊢ ¬ ∀x ¬ x = y

Proof of Theorem ax-9

Step	Hyp	Ref	Expression
1		ax-i9 1417	. . 3 ⊢ ∃x x = y
2	1	notnoti 553	. 2 ⊢ ¬ ¬ ∃x x = y
3		alnex 1380	. 2 ⊢ (∀x ¬ x = y ↔ ¬ ∃x x = y)
4	2, 3	mtbir 575	1 ⊢ ¬ ∀x ¬ x = y

Syntax hints:  ¬ wn 3  ∀wal 1335  ∃wex 1374   = wceq 1383

This theorem is referenced by:  equidqe  1419  equidqeOLD  1420  ax4  1423

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-in1 527  ax-in2 528  ax-5 1336  ax-gen 1339  ax-ie2 1376  ax-i9 1417

This theorem depends on definitions:  df-bi 109  df-tru 1313  df-fal 1314