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

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

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

See also the remarks for ax9v 1636 and ax9 1889. This theorem does not actually use ax9v 1636 so that other paths to ax9 1889 can be demonstrated (such as in ax9sep 29160). Theorem ax9 1889 uses this one to make the derivation from ax9v 1636. (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 29142 . . 3  |-  ( A. x  -.  x  =  y  ->  -.  x  =  y )
41, 2ax9lem3 29142 . . 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 1603 . . . 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 29145 . . . . . . 7  |-  -.  A. z  -.  z  =  v
198, 9, 10, 11, 1, 12, 13, 2, 14, 15, 16, 18ax9lem18 29157 . . . . . 6  |-  ( -. 
A. x  x  =  y  ->  ( v  =  y  ->  A. x  v  =  y )
)
201, 2ax9lem7 29146 . . . . . . . . 9  |-  ( A. x  v  =  y  ->  A. x A. x  v  =  y )
211, 2ax9lem3 29142 . . . . . . . . . 10  |-  ( A. x  v  =  y  ->  v  =  y )
221ax9lem1 29140 . . . . . . . . . . . . 13  |-  ( x  =  v  ->  v  =  x )
23 ax-8 1643 . . . . . . . . . . . . 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 1550 . . . . . . . 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 1552 . . 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 1527
This theorem is referenced by:  ax9OLD  29159  ax9sep  29160
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