Metamath Proof Explorer

Theorem nel1nelin

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

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

Proof

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