Metamath Proof Explorer


Theorem elrint

Description: Membership in a restricted intersection. (Contributed by Stefan O'Rear, 3-Apr-2015)

Ref Expression
Assertion elrint X A B X A y B X y

Proof

Step Hyp Ref Expression
1 elin X A B X A X B
2 elintg X A X B y B X y
3 2 pm5.32i X A X B X A y B X y
4 1 3 bitri X A B X A y B X y