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  2094  ax4567  26767  a9e2nd  27017  a9e2ndVD  27374  a9e2ndALT  27397  a12study9  27809  ax10lem17ALT  27812  ax9lem4  27832  ax9lem7  27835  ax9lem8  27836  ax9lem9  27837  ax9lem17  27845
  Copyright terms: Public domain W3C validator