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.)