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

Theorem a12stdy2-x12 29112
Description: Part of a study related to ax12o 1875. Weak version of a12stdy2 29127. Does not use sp 1716, ax9 1889, ax10 1884, or ax12o 1875 but allows ax9v 1636. The consequent is quantified with a different variable. (Contributed by NM, 7-Nov-1015.) (Proof modification is discouraged.) (New usage is discouraged.)
Assertion
Ref Expression
a12stdy2-x12  |-  ( A. z ( z  =  x  /\  x  =  y )  ->  A. y 
y  =  x )
Distinct variable group:    y, z

Proof of Theorem a12stdy2-x12
StepHypRef Expression
1 equequ2 1649 . . . . 5  |-  ( x  =  y  ->  (
z  =  x  <->  z  =  y ) )
21biimpd 198 . . . 4  |-  ( x  =  y  ->  (
z  =  x  -> 
z  =  y ) )
32imdistanri 672 . . 3  |-  ( ( z  =  x  /\  x  =  y )  ->  ( z  =  y  /\  x  =  y ) )
43alimi 1546 . 2  |-  ( A. z ( z  =  x  /\  x  =  y )  ->  A. z
( z  =  y  /\  x  =  y ) )
5 19.26 1580 . . 3  |-  ( A. z ( z  =  y  /\  x  =  y )  <->  ( A. z  z  =  y  /\  A. z  x  =  y ) )
6 ax10lem3 1878 . . . . 5  |-  ( A. z  z  =  y  ->  A. y  y  =  z )
7 ax10lem6 1883 . . . . . 6  |-  ( A. y  y  =  z  ->  ( A. z  x  =  y  ->  A. y  x  =  y )
)
8 equcomi 1646 . . . . . . 7  |-  ( x  =  y  ->  y  =  x )
98alimi 1546 . . . . . 6  |-  ( A. y  x  =  y  ->  A. y  y  =  x )
107, 9syl6 29 . . . . 5  |-  ( A. y  y  =  z  ->  ( A. z  x  =  y  ->  A. y 
y  =  x ) )
116, 10syl 15 . . . 4  |-  ( A. z  z  =  y  ->  ( A. z  x  =  y  ->  A. y 
y  =  x ) )
1211imp 418 . . 3  |-  ( ( A. z  z  =  y  /\  A. z  x  =  y )  ->  A. y  y  =  x )
135, 12sylbi 187 . 2  |-  ( A. z ( z  =  y  /\  x  =  y )  ->  A. y 
y  =  x )
144, 13syl 15 1  |-  ( A. z ( z  =  x  /\  x  =  y )  ->  A. y 
y  =  x )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 358   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-11 1715
This theorem depends on definitions:  df-bi 177  df-an 360  df-ex 1529
  Copyright terms: Public domain W3C validator