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	⊢ ( 𝜑 → 𝑋 ∈ ( 𝐴 ∩ 𝐵 ) )