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

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

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

See also the remarks for ax9v 1662 and ax9 1942. This theorem does not actually use ax9v 1662 so that other paths to ax9 1942 can be demonstrated (such as in ax9sep 29136). Theorem ax9 1942 uses this one to make the derivation from ax9v 1662. (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 29118 . . 3  |-  ( A. x  -.  x  =  y  ->  -.  x  =  y )
41, 2ax9lem3 29118 . . 3  |-  ( A. x  x  =  y  ->  x  =  y )
53, 4nsyl3 113 . 2  |-  ( A. x  x  =  y  ->  -.  A. x  -.  x  =  y )
6 ax9vax9.z . . 3  |-  -.  A. v  -.  v  =  y
7 ax-17 1623 . . . 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 29121 . . . . . . 7  |-  -.  A. z  -.  z  =  v
198, 9, 10, 11, 1, 12, 13, 2, 14, 15, 16, 18ax9lem18 29133 . . . . . 6  |-  ( -. 
A. x  x  =  y  ->  ( v  =  y  ->  A. x  v  =  y )
)
201, 2ax9lem7 29122 . . . . . . . . 9  |-  ( A. x  v  =  y  ->  A. x A. x  v  =  y )
211, 2ax9lem3 29118 . . . . . . . . . 10  |-  ( A. x  v  =  y  ->  v  =  y )
221ax9lem1 29116 . . . . . . . . . . . . 13  |-  ( x  =  v  ->  v  =  x )
23 ax-8 1682 . . . . . . . . . . . . 13  |-  ( v  =  x  ->  (
v  =  y  ->  x  =  y )
)
2422, 23syl 16 . . . . . . . . . . . 12  |-  ( x  =  v  ->  (
v  =  y  ->  x  =  y )
)
2524com12 29 . . . . . . . . . . 11  |-  ( v  =  y  ->  (
x  =  v  ->  x  =  y )
)
2625con3d 127 . . . . . . . . . 10  |-  ( v  =  y  ->  ( -.  x  =  y  ->  -.  x  =  v ) )
2721, 26syl 16 . . . . . . . . 9  |-  ( A. x  v  =  y  ->  ( -.  x  =  y  ->  -.  x  =  v ) )
2820, 27alimdh 1569 . . . . . . . 8  |-  ( A. x  v  =  y  ->  ( A. x  -.  x  =  y  ->  A. x  -.  x  =  v ) )
2928con3d 127 . . . . . . 7  |-  ( A. x  v  =  y  ->  ( -.  A. x  -.  x  =  v  ->  -.  A. x  -.  x  =  y )
)
3017, 29mpi 17 . . . . . 6  |-  ( A. x  v  =  y  ->  -.  A. x  -.  x  =  y )
3119, 30syl6com 33 . . . . 5  |-  ( v  =  y  ->  ( -.  A. x  x  =  y  ->  -.  A. x  -.  x  =  y
) )
3231con3i 129 . . . 4  |-  ( -.  ( -.  A. x  x  =  y  ->  -. 
A. x  -.  x  =  y )  ->  -.  v  =  y
)
337, 32alrimih 1571 . . 3  |-  ( -.  ( -.  A. x  x  =  y  ->  -. 
A. x  -.  x  =  y )  ->  A. v  -.  v  =  y )
346, 33mt3 173 . 2  |-  ( -. 
A. x  x  =  y  ->  -.  A. x  -.  x  =  y
)
355, 34pm2.61i 158 1  |-  -.  A. x  -.  x  =  y
Colors of variables: wff set class
Syntax hints:   -. wn 3    -> wi 4   A.wal 1546
This theorem is referenced by:  ax9OLD  29135  ax9sep  29136
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1661  ax-8 1682  ax-6 1736  ax-7 1741  ax-11 1753  ax-12 1939
This theorem depends on definitions:  df-bi 178  df-an 361  df-ex 1548  df-nf 1551
  Copyright terms: Public domain W3C validator