Metamath Proof Explorer

Theorem nel2nelin

Description: Membership in an intersection implies membership in the second set. (Contributed by Glauco Siliprandi, 2-Jan-2022)

Ref Expression
Assertion nel2nelin 
|- ( -. A e. C -> -. A e. ( B i^i C ) )

Proof

Step Hyp Ref Expression
1 elinel2 
 |-  ( A e. ( B i^i C ) -> A e. C )
2 1 con3i 
 |-  ( -. A e. C -> -. A e. ( B i^i C ) )