Metamath Proof Explorer

Theorem nalfal

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

Ref Expression
Assertion nalfal 
|- -. A. x F.

Proof

Step Hyp Ref Expression
1 alfal 
 |-  A. x -. F.
2 falim 
 |-  ( F. -> -. A. x -. F. )
3 2 sps 
 |-  ( A. x F. -> -. A. x -. F. )
4 1 3 mt2 
 |-  -. A. x F.