Metamath Proof Explorer


Theorem elinti

Description: Membership in class intersection. (Contributed by NM, 14-Oct-1999) (Proof shortened by Andrew Salmon, 9-Jul-2011)

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

Proof

Step Hyp Ref Expression
1 elintg
 |-  ( A e. |^| B -> ( A e. |^| B <-> A. x e. B A e. x ) )
2 eleq2
 |-  ( x = C -> ( A e. x <-> A e. C ) )
3 2 rspccv
 |-  ( A. x e. B A e. x -> ( C e. B -> A e. C ) )
4 1 3 syl6bi
 |-  ( A e. |^| B -> ( A e. |^| B -> ( C e. B -> A e. C ) ) )
5 4 pm2.43i
 |-  ( A e. |^| B -> ( C e. B -> A e. C ) )