Metamath Proof Explorer


Theorem nalfal

Description: Not all sets hold F. as true. (Contributed by Anthony Hart, 13-Sep-2011)

Ref Expression
Assertion nalfal ¬x

Proof

Step Hyp Ref Expression
1 alfal x¬
2 falim ¬x¬
3 2 sps x¬x¬
4 1 3 mt2 ¬x