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

Axiom ax-6 1534
Description: Axiom of Quantified Negation. Axiom C5-2 of [Monk2] p. 113. (Contributed by NM, 5-Aug-1993.)
Assertion
Ref Expression
ax-6  |-  ( -. 
A. x ph  ->  A. x  -.  A. x ph )

Detailed syntax breakdown of Axiom ax-6
StepHypRef Expression
1 wph . . . 4  wff  ph
2 vx . . . 4  set  x
31, 2wal 1532 . . 3  wff  A. x ph
43wn 5 . 2  wff  -.  A. x ph
54, 2wal 1532 . 2  wff  A. x  -.  A. x ph
64, 5wi 6 1  wff  ( -. 
A. x ph  ->  A. x  -.  A. x ph )
Colors of variables: wff set class
This axiom is referenced by:  hbn1  1564  ax12o10lem5  1639  ax12o10lem6  1640  ax12o10lem7  1641  ax12o10lem9  1643  ax10lem24  1673  equidq  1689  ax5o  1693  ax6o  1696  hba1  1718  ax9o  1814  dvelimALT  2097  ax4567  26954  a9e2nd  27361  a9e2ndVD  27718  a9e2ndALT  27741  ax12o10lem5X  28190  ax12o10lem6X  28192  ax12o10lem7X  28194  ax12o10lem9X  28199  ax10lem24X  28244  a12study9  28271  ax10lem17ALT  28274  ax9lem4  28294  ax9lem7  28297  ax9lem8  28298  ax9lem9  28299  ax9lem17  28307
  Copyright terms: Public domain W3C validator