bv-∀

Theorem.

Arguments:

y (sv), phi (pr), x (sv),

Hypotheses:

(x bound in phi)

Assertions:

(x bound in forallyphi)

Proof:

Hyp Ref Line Expr
Hypo1(x bound in phi)
1df-Bvp2(phitoforallxphi)
2fv-aly3(forallyphitoforallxforallyphi)
3df-Bvp4(x bound in forallyphi)