Theorem elint

Description: Membership in class intersection. (Contributed by NM, 21-May-1994)

	Ref	Expression
Hypothesis	elint.1	|- A e. _V
Assertion	elint	|- ( A e. |^| B <-> A. x ( x e. B -> A e. x ) )

Proof

Step	Hyp	Ref	Expression
1		elint.1	|- A e. _V
2		eleq1	|- ( y = A -> ( y e. x <-> A e. x ) )
3	2	imbi2d	|- ( y = A -> ( ( x e. B -> y e. x ) <-> ( x e. B -> A e. x ) ) )
4	3	albidv	|- ( y = A -> ( A. x ( x e. B -> y e. x ) <-> A. x ( x e. B -> A e. x ) ) )
5		df-int	|- |^| B = { y | A. x ( x e. B -> y e. x ) }
6	4 5	elab2g	|- ( A e. _V -> ( A e. |^| B <-> A. x ( x e. B -> A e. x ) ) )
7	1 6	ax-mp	|- ( A e. |^| B <-> A. x ( x e. B -> A e. x ) )