Metamath Proof Explorer

Theorem fileln0

Description: An element of a filter is nonempty. (Contributed by FL, 24-May-2011) (Revised by Mario Carneiro, 28-Jul-2015)

Ref Expression
Assertion fileln0 
|- ( ( F e. ( Fil ` X ) /\ A e. F ) -> A =/= (/) )

Proof

Step Hyp Ref Expression
1 id 
 |-  ( A e. F -> A e. F )
2 0nelfil 
 |-  ( F e. ( Fil ` X ) -> -. (/) e. F )
3 nelne2 
 |-  ( ( A e. F /\ -. (/) e. F ) -> A =/= (/) )
4 1 2 3 syl2anr 
 |-  ( ( F e. ( Fil ` X ) /\ A e. F ) -> A =/= (/) )