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  27114  a9e2ndVD  27471  a9e2ndALT  27494  ax12o10lem5X  27943  ax12o10lem6X  27945  ax12o10lem7X  27947  ax12o10lem9X  27952  ax10lem24X  27997  a12study9  28024  ax10lem17ALT  28027  ax9lem4  28047  ax9lem7  28050  ax9lem8  28051  ax9lem9  28052  ax9lem17  28060
  Copyright terms: Public domain W3C validator