This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 )