Theorem elin2

Description: Membership in a class defined as an intersection. (Contributed by Stefan O'Rear, 29-Mar-2015)

	Ref	Expression
Hypothesis	elin2.x	⊢ 𝑋 = ( 𝐵 ∩ 𝐶 )
Assertion	elin2	⊢ ( 𝐴 ∈ 𝑋 ↔ ( 𝐴 ∈ 𝐵 ∧ 𝐴 ∈ 𝐶 ) )

Proof

Step	Hyp	Ref	Expression
1		elin2.x	⊢ 𝑋 = ( 𝐵 ∩ 𝐶 )
2	1	eleq2i	⊢ ( 𝐴 ∈ 𝑋 ↔ 𝐴 ∈ ( 𝐵 ∩ 𝐶 ) )
3		elin	⊢ ( 𝐴 ∈ ( 𝐵 ∩ 𝐶 ) ↔ ( 𝐴 ∈ 𝐵 ∧ 𝐴 ∈ 𝐶 ) )
4	2 3	bitri	⊢ ( 𝐴 ∈ 𝑋 ↔ ( 𝐴 ∈ 𝐵 ∧ 𝐴 ∈ 𝐶 ) )