MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  ax12o10lem1 Unicode version

Theorem ax12o10lem1 1635
Description: Lemma for ax12o 1663 and ax10 1677. Same as equcomi 1822, without using ax-4 1692, ax-9 1684, ax-10 1678, or ax-12o 1664 but allowing ax-9v 1632.

Note that in these lemmas we use ax-9v 1632 instead of ax-9 1684 since the proof of ax9 1683 from ax-9v 1632 makes use of ax-12o 1664. The first use of ax-12o 1664 occurs in ax10lem24 1673. (Contributed by NM, 25-Jul-2015.) (New usage is discouraged.)

Assertion
Ref Expression
ax12o10lem1  |-  ( x  =  y  ->  y  =  x )

Proof of Theorem ax12o10lem1
StepHypRef Expression
1 ax-9v 1632 . . . 4  |-  -.  A. w  -.  w  =  x
2 ax-8 1623 . . . . . . 7  |-  ( w  =  x  ->  (
w  =  x  ->  x  =  x )
)
32pm2.43i 45 . . . . . 6  |-  ( w  =  x  ->  x  =  x )
43con3i 129 . . . . 5  |-  ( -.  x  =  x  ->  -.  w  =  x
)
54alimi 1546 . . . 4  |-  ( A. w  -.  x  =  x  ->  A. w  -.  w  =  x )
61, 5mto 169 . . 3  |-  -.  A. w  -.  x  =  x
7 ax-17 1628 . . 3  |-  ( -.  x  =  x  ->  A. w  -.  x  =  x )
86, 7mt3 173 . 2  |-  x  =  x
9 ax-8 1623 . 2  |-  ( x  =  y  ->  (
x  =  x  -> 
y  =  x ) )
108, 9mpi 18 1  |-  ( x  =  y  ->  y  =  x )
Colors of variables: wff set class
Syntax hints:   -. wn 5    -> wi 6   A.wal 1532
This theorem is referenced by:  ax12o10lem2  1636  ax12o10lem3  1637  ax12olem21  1655  ax12olem26  1660  ax12olem27  1661  ax10lem16  1665  ax10  1677  a16gALT  1679  ax12o10lem2X  27834  ax12o10lem3X  27835  ax12olem21X  27873  ax12olem26X  27882  ax12olem27X  27883  ax10lem16X  27886  ax10X  27898  a16gALTX  27899  hbae-x12  27910  a12stdy2-x12  27913  equvinv  27915  equvelv  27917  ax10lem18ALT  27925  a12study10n  27938
This theorem was proved from axioms:  ax-1 7  ax-2 8  ax-3 9  ax-mp 10  ax-5 1533  ax-gen 1536  ax-8 1623  ax-17 1628  ax-9v 1632
  Copyright terms: Public domain W3C validator