Metamath Proof Explorer
Description: Elementhood in the first set of an intersection  deduction version.
(Contributed by Thierry Arnoux, 3May2020)


Ref 
Expression 

Hypothesis 
elin1d.1 
⊢ ( 𝜑 → 𝑋 ∈ ( 𝐴 ∩ 𝐵 ) ) 

Assertion 
elin2d 
⊢ ( 𝜑 → 𝑋 ∈ 𝐵 ) 
Proof
Step 
Hyp 
Ref 
Expression 
1 

elin1d.1 
⊢ ( 𝜑 → 𝑋 ∈ ( 𝐴 ∩ 𝐵 ) ) 
2 

elinel2 
⊢ ( 𝑋 ∈ ( 𝐴 ∩ 𝐵 ) → 𝑋 ∈ 𝐵 ) 
3 
1 2

syl 
⊢ ( 𝜑 → 𝑋 ∈ 𝐵 ) 