MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  ax-10 Structured version   Visualization version   GIF version

Axiom ax-10 1965
Description: Axiom of Quantified Negation. Axiom C5-2 of [Monk2] p. 113. This axiom scheme is logically redundant (see ax10w 1953) but is used as an auxiliary axiom scheme to achieve metalogical completeness. It means that 𝑥 is not free in ¬ ∀𝑥𝜑. (Contributed by NM, 21-May-2008.) Use its alias hbn1 1966 instead if you must use it. Any theorem in first order logic (FOL) that contains only set variables that are all mutually distinct, and has no wff variables, can be proved *without* using ax-10 1965 through ax-13 2137, by invoking ax10w 1953 through ax13w 1960. We encourage proving theorems *without* ax-10 1965 through ax-13 2137 and moving them up to the ax-4 1711 through ax-9 1946 section. (New usage is discouraged.)
Assertion
Ref Expression
ax-10 (¬ ∀𝑥𝜑 → ∀𝑥 ¬ ∀𝑥𝜑)

Detailed syntax breakdown of Axiom ax-10
StepHypRef Expression
1 wph . . . 4 wff 𝜑
2 vx . . . 4 setvar 𝑥
31, 2wal 1466 . . 3 wff 𝑥𝜑
43wn 3 . 2 wff ¬ ∀𝑥𝜑
54, 2wal 1466 . 2 wff 𝑥 ¬ ∀𝑥𝜑
64, 5wi 4 1 wff (¬ ∀𝑥𝜑 → ∀𝑥 ¬ ∀𝑥𝜑)
Colors of variables: wff setvar class
This axiom is referenced by:  hbn1  1966
  Copyright terms: Public domain W3C validator