# Metamath Proof Explorer

## Axiom ax-10

Description: Axiom of Quantified Negation. Axiom C5-2 of Monk2 p. 113. This axiom scheme is logically redundant (see ax10w ) but is used as an auxiliary axiom scheme to achieve scheme completeness. It means that x is not free in -. A. x ph . (Contributed by NM, 21-May-2008) Use its alias hbn1 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 through ax-13 , by invoking ax10w through ax13w . We encourage proving theorems *without* ax-10 through ax-13 and moving them up to the ax-4 through ax-9 section. (New usage is discouraged.)

Ref Expression
Assertion ax-10 ${⊢}¬\forall {x}\phantom{\rule{.4em}{0ex}}{\phi }\to \forall {x}\phantom{\rule{.4em}{0ex}}¬\forall {x}\phantom{\rule{.4em}{0ex}}{\phi }$

### Detailed syntax breakdown

Step Hyp Ref Expression
0 vx ${setvar}{x}$
1 wph ${wff}{\phi }$
2 1 0 wal ${wff}\forall {x}\phantom{\rule{.4em}{0ex}}{\phi }$
3 2 wn ${wff}¬\forall {x}\phantom{\rule{.4em}{0ex}}{\phi }$
4 3 0 wal ${wff}\forall {x}\phantom{\rule{.4em}{0ex}}¬\forall {x}\phantom{\rule{.4em}{0ex}}{\phi }$
5 3 4 wi ${wff}\left(¬\forall {x}\phantom{\rule{.4em}{0ex}}{\phi }\to \forall {x}\phantom{\rule{.4em}{0ex}}¬\forall {x}\phantom{\rule{.4em}{0ex}}{\phi }\right)$