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  28163  ax12o10lem3X  28164  ax12olem21X  28202  ax12olem26X  28211  ax12olem27X  28212  ax10lem16X  28215  ax10X  28227  a16gALTX  28228  hbae-x12  28239  a12stdy2-x12  28242  equvinv  28244  equvelv  28246  ax10lem18ALT  28254  a12study10n  28267
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