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

Theorem ax10o 2038
Description: Show that ax-10o 2215 can be derived from ax-10 2216 in the form of ax10 2025. Normally, ax10o 2038 should be used rather than ax-10o 2215, except by theorems specifically studying the latter's properties. (Contributed by NM, 16-May-2008.) (Proof shortened by Wolf Lammen, 21-Apr-2018.)
Assertion
Ref Expression
ax10o  |-  ( A. x  x  =  y  ->  ( A. x ph  ->  A. y ph )
)

Proof of Theorem ax10o
StepHypRef Expression
1 ax10o2 2024 . 2  |-  ( A. y  y  =  x  ->  ( A. x ph  ->  A. y ph )
)
21aecoms 2036 1  |-  ( A. x  x  =  y  ->  ( A. x ph  ->  A. y ph )
)
Colors of variables: wff set class
Syntax hints:    -> wi 4   A.wal 1549
This theorem is referenced by:  hbae  2040  hbaeOLD  2041  a16g  2048  dral1  2053  dral1OLD  2054  dvelimhOLD  2068  nd1  8452  nd2  8453  axpowndlem3  8464  a9e2eq  28545  a9e2eqVD  28920  2sb5ndVD  28923  2sb5ndALT  28945
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1555  ax-5 1566  ax-17 1626  ax-9 1666  ax-8 1687  ax-6 1744  ax-7 1749  ax-11 1761  ax-12 1950
This theorem depends on definitions:  df-bi 178  df-an 361  df-ex 1551  df-nf 1554
  Copyright terms: Public domain W3C validator