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 ABCBAC

Proof

Step Hyp Ref Expression
1 elintg ABABxBAx
2 eleq2 x=CAxAC
3 2 rspccv xBAxCBAC
4 1 3 syl6bi ABABCBAC
5 4 pm2.43i ABCBAC