fv-exy

Theorem.

Arguments:

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

Hypotheses:

(phitoforallxphi)

Assertions:

(existsyphitoforallxexistsyphi)

Proof:

Hyp Ref Line Expr
Hypo1(phitoforallxphi)
1fv-neg2(lnotphitoforallxlnotphi)
2fv-aly3(forallylnotphitoforallxforallylnotphi)
3fv-neg4(lnotforallylnotphitoforallxlnotforallylnotphi)
df-ex5(existsyphileftrightarrowlnotforallylnotphi)
5eqt-∀-i6(forallxexistsyphileftrightarrowforallxlnotforallylnotphi)
4, 5, 6<imtr7(existsyphitoforallxexistsyphi)