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

Theorem ax9vax9 29780
Description: Derive ax9 1902 (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 1902 nor sp 1728 (which can be derived from ax9 1902) is used by the proof.

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

See also the remarks for ax9v 1645 and ax9 1902. This theorem does not actually use ax9v 1645 so that other paths to ax9 1902 can be demonstrated (such as in ax9sep 29782). Theorem ax9 1902 uses this one to make the derivation from ax9v 1645. (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 29764 . . 3  |-  ( A. x  -.  x  =  y  ->  -.  x  =  y )
41, 2ax9lem3 29764 . . 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 1606 . . . 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 29767 . . . . . . 7  |-  -.  A. z  -.  z  =  v
198, 9, 10, 11, 1, 12, 13, 2, 14, 15, 16, 18ax9lem18 29779 . . . . . 6  |-  ( -. 
A. x  x  =  y  ->  ( v  =  y  ->  A. x  v  =  y )
)
201, 2ax9lem7 29768 . . . . . . . . 9  |-  ( A. x  v  =  y  ->  A. x A. x  v  =  y )
211, 2ax9lem3 29764 . . . . . . . . . 10  |-  ( A. x  v  =  y  ->  v  =  y )
221ax9lem1 29762 . . . . . . . . . . . . 13  |-  ( x  =  v  ->  v  =  x )
23 ax-8 1661 . . . . . . . . . . . . 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 1553 . . . . . . . 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 1555 . . 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 1530
This theorem is referenced by:  ax9OLD  29781  ax9sep  29782
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1536  ax-5 1547  ax-17 1606  ax-9 1644  ax-8 1661  ax-6 1715  ax-7 1720  ax-11 1727  ax-12 1878
This theorem depends on definitions:  df-bi 177  df-an 360  df-ex 1532
  Copyright terms: Public domain W3C validator