NF weak partition development: NominalLoweringDerived.
Logical wrappers whose Metamath freshness condition follows directly from the nominal free-variable computation. Keeping them separate from the generic lowering theorem makes the source emitter's primitive table small and explicit.
def
NFChoice.DirectNominalPrf.Nominal.ax6
(x : SemanticCore.Var)
(p : SemanticCore.Wff)
:
NPrf ((SemanticCore.Wff.all x p).neg.imp (SemanticCore.Wff.all x (SemanticCore.Wff.all x p).neg))
Metamath ax-6: x is not free in ¬ ∀ x, p.