Metamath Proof Explorer


Theorem elin1d

Description: Elementhood in the first set of an intersection - deduction version. (Contributed by Thierry Arnoux, 3-May-2020)

Ref Expression
Hypothesis elin1d.1
|- ( ph -> X e. ( A i^i B ) )
Assertion elin1d
|- ( ph -> X e. A )

Proof

Step Hyp Ref Expression
1 elin1d.1
 |-  ( ph -> X e. ( A i^i B ) )
2 elinel1
 |-  ( X e. ( A i^i B ) -> X e. A )
3 1 2 syl
 |-  ( ph -> X e. A )