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

Theorem a12stdy2-x12 29734
Description: Part of a study related to ax12o 1887. Weak version of a12stdy2 29749. Does not use sp 1728, ax9 1902, ax10 1897, or ax12o 1887 but allows ax9v 1645. 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 1669 . . . . 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 1549 . 2  |-  ( A. z ( z  =  x  /\  x  =  y )  ->  A. z
( z  =  y  /\  x  =  y ) )
5 19.26 1583 . . 3  |-  ( A. z ( z  =  y  /\  x  =  y )  <->  ( A. z  z  =  y  /\  A. z  x  =  y ) )
6 ax10lem3 1891 . . . . 5  |-  ( A. z  z  =  y  ->  A. y  y  =  z )
7 ax10lem6 1896 . . . . . 6  |-  ( A. y  y  =  z  ->  ( A. z  x  =  y  ->  A. y  x  =  y )
)
8 equcomi 1664 . . . . . . 7  |-  ( x  =  y  ->  y  =  x )
98alimi 1549 . . . . . 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 1530
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-11 1727
This theorem depends on definitions:  df-bi 177  df-an 360  df-ex 1532
  Copyright terms: Public domain W3C validator