aln.ex

Theorem.

Arguments:

x (sv), phi (pr),

Assertions:

(forallxlnotphileftrightarrowlnotexistsxphi)

Proof:

Hyp Ref Line Expr
df-ex1(existsxphileftrightarrowlnotforallxlnotphi)
1conb>i2(forallxlnotphileftrightarrowlnotexistsxphi)