Users' Mathboxes Mathbox for Norm Megill < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  ax9OLD Unicode version

Theorem ax9OLD 29159
Description: Theorem showing that ax9 1889 follows from the weaker version ax9v 1636.

See also ax9 1889 for a slightly more direct proof (using lemmas for ax10 1884 derivation).

This theorem normally should not be referenced in any later proof. Instead, the use of ax9 1889 below is preferred, since it is easier to work with (it has no distinct variable conditions) and it is the standard version we have adopted. (Contributed by NM, 7-Aug-2015.) (Proof modification is discouraged.) (New usage is discouraged.)

Assertion
Ref Expression
ax9OLD  |-  -.  A. x  -.  x  =  y

Proof of Theorem ax9OLD
Dummy variables  u  t  v  w  z are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 ax9v 1636 . 2  |-  -.  A. t  -.  t  =  u
2 ax9v 1636 . 2  |-  -.  A. t  -.  t  =  z
3 ax9v 1636 . 2  |-  -.  A. u  -.  u  =  x
4 ax9v 1636 . 2  |-  -.  A. u  -.  u  =  w
5 ax9v 1636 . 2  |-  -.  A. z  -.  z  =  x
6 ax9v 1636 . 2  |-  -.  A. z  -.  z  =  w
7 ax9v 1636 . 2  |-  -.  A. x  -.  x  =  t
8 ax9v 1636 . 2  |-  -.  A. x  -.  x  =  z
9 ax9v 1636 . 2  |-  -.  A. w  -.  w  =  t
10 ax9v 1636 . 2  |-  -.  A. w  -.  w  =  z
11 ax9v 1636 . 2  |-  -.  A. w  -.  w  =  y
12 ax9v 1636 . 2  |-  -.  A. x  -.  x  =  v
13 ax9v 1636 . 2  |-  -.  A. v  -.  v  =  y
141, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11, 12, 13ax9vax9 29158 1  |-  -.  A. x  -.  x  =  y
Colors of variables: wff set class
Syntax hints:   -. wn 3   A.wal 1527
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1533  ax-5 1544  ax-17 1603  ax-9 1635  ax-8 1643  ax-6 1703  ax-7 1708  ax-11 1715  ax-12 1866
This theorem depends on definitions:  df-bi 177  df-an 360  df-ex 1529
  Copyright terms: Public domain W3C validator