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

Theorem ax9vax9 29231
Description: Derive ax9 1891 (which has no distinct variable requirement) from a weaker version that requires that its two variables be distinct. The weaker version is axiom scheme B7 of [Tarski] p. 75. The hypotheses are the instances of the weaker version that we need. Neither ax9 1891 nor sp 1718 (which can be derived from ax9 1891) is used by the proof.

Revised on 7-Aug-2015 to remove the dependence on ax10 1886.

See also the remarks for ax9v 1638 and ax9 1891. This theorem does not actually use ax9v 1638 so that other paths to ax9 1891 can be demonstrated (such as in ax9sep 29233). Theorem ax9 1891 uses this one to make the derivation from ax9v 1638. (Contributed by NM, 12-Nov-2013.) (Revised by NM, 7-Aug-2015.) (Proof modification is discouraged.) (New usage is discouraged.)

Hypotheses
Ref Expression
ax9vax9.a  |-  -.  A. t  -.  t  =  u
ax9vax9.b  |-  -.  A. t  -.  t  =  z
ax9vax9.e  |-  -.  A. u  -.  u  =  x
ax9vax9.f  |-  -.  A. u  -.  u  =  w
ax9vax9.i  |-  -.  A. z  -.  z  =  x
ax9vax9.j  |-  -.  A. z  -.  z  =  w
ax9vax9.k  |-  -.  A. x  -.  x  =  t
ax9vax9.m  |-  -.  A. x  -.  x  =  z
ax9vax9.p  |-  -.  A. w  -.  w  =  t
ax9vax9.r  |-  -.  A. w  -.  w  =  z
ax9vax9.t  |-  -.  A. w  -.  w  =  y
ax9vax9.y  |-  -.  A. x  -.  x  =  v
ax9vax9.z  |-  -.  A. v  -.  v  =  y
Assertion
Ref Expression
ax9vax9  |-  -.  A. x  -.  x  =  y
Distinct variable groups:    u, t, w, x, v, z    y, u, w, v, z

Proof of Theorem ax9vax9
StepHypRef Expression
1 ax9vax9.i . . . 4  |-  -.  A. z  -.  z  =  x
2 ax9vax9.m . . . 4  |-  -.  A. x  -.  x  =  z
31, 2ax9lem3 29215 . . 3  |-  ( A. x  -.  x  =  y  ->  -.  x  =  y )
41, 2ax9lem3 29215 . . 3  |-  ( A. x  x  =  y  ->  x  =  y )
53, 4nsyl3 111 . 2  |-  ( A. x  x  =  y  ->  -.  A. x  -.  x  =  y )
6 ax9vax9.z . . 3  |-  -.  A. v  -.  v  =  y
7 ax-17 1605 . . . 4  |-  ( -.  ( -.  A. x  x  =  y  ->  -. 
A. x  -.  x  =  y )  ->  A. v  -.  ( -.  A. x  x  =  y  ->  -.  A. x  -.  x  =  y
) )
8 ax9vax9.a . . . . . . 7  |-  -.  A. t  -.  t  =  u
9 ax9vax9.b . . . . . . 7  |-  -.  A. t  -.  t  =  z
10 ax9vax9.e . . . . . . 7  |-  -.  A. u  -.  u  =  x
11 ax9vax9.f . . . . . . 7  |-  -.  A. u  -.  u  =  w
12 ax9vax9.j . . . . . . 7  |-  -.  A. z  -.  z  =  w
13 ax9vax9.k . . . . . . 7  |-  -.  A. x  -.  x  =  t
14 ax9vax9.p . . . . . . 7  |-  -.  A. w  -.  w  =  t
15 ax9vax9.r . . . . . . 7  |-  -.  A. w  -.  w  =  z
16 ax9vax9.t . . . . . . 7  |-  -.  A. w  -.  w  =  y
17 ax9vax9.y . . . . . . . 8  |-  -.  A. x  -.  x  =  v
1815, 12, 1, 17ax9lem6 29218 . . . . . . 7  |-  -.  A. z  -.  z  =  v
198, 9, 10, 11, 1, 12, 13, 2, 14, 15, 16, 18ax9lem18 29230 . . . . . 6  |-  ( -. 
A. x  x  =  y  ->  ( v  =  y  ->  A. x  v  =  y )
)
201, 2ax9lem7 29219 . . . . . . . . 9  |-  ( A. x  v  =  y  ->  A. x A. x  v  =  y )
211, 2ax9lem3 29215 . . . . . . . . . 10  |-  ( A. x  v  =  y  ->  v  =  y )
221ax9lem1 29213 . . . . . . . . . . . . 13  |-  ( x  =  v  ->  v  =  x )
23 ax-8 1645 . . . . . . . . . . . . 13  |-  ( v  =  x  ->  (
v  =  y  ->  x  =  y )
)
2422, 23syl 15 . . . . . . . . . . . 12  |-  ( x  =  v  ->  (
v  =  y  ->  x  =  y )
)
2524com12 27 . . . . . . . . . . 11  |-  ( v  =  y  ->  (
x  =  v  ->  x  =  y )
)
2625con3d 125 . . . . . . . . . 10  |-  ( v  =  y  ->  ( -.  x  =  y  ->  -.  x  =  v ) )
2721, 26syl 15 . . . . . . . . 9  |-  ( A. x  v  =  y  ->  ( -.  x  =  y  ->  -.  x  =  v ) )
2820, 27alimdh 1552 . . . . . . . 8  |-  ( A. x  v  =  y  ->  ( A. x  -.  x  =  y  ->  A. x  -.  x  =  v ) )
2928con3d 125 . . . . . . 7  |-  ( A. x  v  =  y  ->  ( -.  A. x  -.  x  =  v  ->  -.  A. x  -.  x  =  y )
)
3017, 29mpi 16 . . . . . 6  |-  ( A. x  v  =  y  ->  -.  A. x  -.  x  =  y )
3119, 30syl6com 31 . . . . 5  |-  ( v  =  y  ->  ( -.  A. x  x  =  y  ->  -.  A. x  -.  x  =  y
) )
3231con3i 127 . . . 4  |-  ( -.  ( -.  A. x  x  =  y  ->  -. 
A. x  -.  x  =  y )  ->  -.  v  =  y
)
337, 32alrimih 1554 . . 3  |-  ( -.  ( -.  A. x  x  =  y  ->  -. 
A. x  -.  x  =  y )  ->  A. v  -.  v  =  y )
346, 33mt3 171 . 2  |-  ( -. 
A. x  x  =  y  ->  -.  A. x  -.  x  =  y
)
355, 34pm2.61i 156 1  |-  -.  A. x  -.  x  =  y
Colors of variables: wff set class
Syntax hints:   -. wn 3    -> wi 4   A.wal 1529
This theorem is referenced by:  ax9OLD  29232  ax9sep  29233
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1535  ax-5 1546  ax-17 1605  ax-9 1637  ax-8 1645  ax-6 1705  ax-7 1710  ax-11 1717  ax-12 1868
This theorem depends on definitions:  df-bi 177  df-an 360  df-ex 1531
  Copyright terms: Public domain W3C validator