bv-¬

Theorem.

Arguments:

phi (pr), x (sv),

Hypotheses:

(x bound in phi)

Assertions:

(x bound in lnotphi)

Proof:

Hyp Ref Line Expr
Hypo1(x bound in phi)
1df-Bvp2(phitoforallxphi)
2fv-neg3(lnotphitoforallxlnotphi)
3df-Bvp4(x bound in lnotphi)