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

Theorem ax9 1953
 Description: Theorem showing that ax-9 1666 follows from the weaker version ax9v 1667. (Even though this theorem depends on ax-9 1666, all references of ax-9 1666 are made via ax9v 1667. An earlier version stated ax9v 1667 as a separate axiom, but having two axioms caused some confusion.) This theorem should be referenced in place of ax-9 1666 so that all proofs can be traced back to ax9v 1667. (Contributed by NM, 12-Nov-2013.) (Revised by NM, 25-Jul-2015.) (Proof shortened by Wolf Lammen, 4-Feb-2018.)
Assertion
Ref Expression
ax9

Proof of Theorem ax9
StepHypRef Expression
1 a9e 1952 . 2
2 df-ex 1551 . 2
31, 2mpbi 200 1
 Colors of variables: wff set class Syntax hints:   wn 3  wal 1549  wex 1550 This theorem is referenced by:  ax9o  1954  a9eOLD  2034  ax4567to4  27534 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-11 1761  ax-12 1950 This theorem depends on definitions:  df-bi 178  df-an 361  df-ex 1551
 Copyright terms: Public domain W3C validator