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  hbae-x12  27798  a12stdy2-x12  27801  equvinv  27803  equvelv  27805  ax10lem18ALT  27813  a12study10n  27826
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