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

Metamath Proof Explorer

Theorem elind

Description: Deduce membership in an intersection of two classes. (Contributed by Jonathan Ben-Naim, 3-Jun-2011)

Ref Expression
Hypotheses elind.1 ⊢ ( 𝜑 → 𝑋 ∈ 𝐴 )
elind.2 ⊢ ( 𝜑 → 𝑋 ∈ 𝐵 )
Assertion elind ( 𝜑 → 𝑋 ∈ ( 𝐴 ∩ 𝐵 ) )

Proof

Step Hyp Ref Expression
1 elind.1 ⊢ ( 𝜑 → 𝑋 ∈ 𝐴 )
2 elind.2 ⊢ ( 𝜑 → 𝑋 ∈ 𝐵 )
3 elin ⊢ ( 𝑋 ∈ ( 𝐴 ∩ 𝐵 ) ↔ ( 𝑋 ∈ 𝐴 ∧ 𝑋 ∈ 𝐵 ) )
4 1 2 3 sylanbrc ⊢ ( 𝜑 → 𝑋 ∈ ( 𝐴 ∩ 𝐵 ) )