Metamath Proof Explorer

Theorem elinel2

Description: Membership in an intersection implies membership in the second set. (Contributed by Glauco Siliprandi, 11-Dec-2019)

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

Proof

Step Hyp Ref Expression
1 elin 
 |-  ( A e. ( B i^i C ) <-> ( A e. B /\ A e. C ) )
2 1 simprbi 
 |-  ( A e. ( B i^i C ) -> A e. C )