Theorem elin2

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

	Ref	Expression
Hypothesis	elin2.x	|- X = ( B i^i C )
Assertion	elin2	|- ( A e. X <-> ( A e. B /\ A e. C ) )

Proof

Step	Hyp	Ref	Expression
1		elin2.x	|- X = ( B i^i C )
2	1	eleq2i	|- ( A e. X <-> A e. ( B i^i C ) )
3		elin	|- ( A e. ( B i^i C ) <-> ( A e. B /\ A e. C ) )
4	2 3	bitri	|- ( A e. X <-> ( A e. B /\ A e. C ) )