Metamath Proof Explorer


Theorem elinel1

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

Ref Expression
Assertion elinel1 A B C A B

Proof

Step Hyp Ref Expression
1 elin A B C A B A C
2 1 simplbi A B C A B