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	|- ( z = y -> ( z e. x <-> y e. x ) )
3	2	imbi2d	|- ( z = y -> ( ( x e. B -> z e. x ) <-> ( x e. B -> y e. x ) ) )
4	3	albidv	|- ( z = y -> ( A. x ( x e. B -> z e. x ) <-> A. x ( x e. B -> y e. x ) ) )
5		eleq1	|- ( y = A -> ( y e. x <-> A e. x ) )
6	5	imbi2d	|- ( y = A -> ( ( x e. B -> y e. x ) <-> ( x e. B -> A e. x ) ) )
7	6	albidv	|- ( y = A -> ( A. x ( x e. B -> y e. x ) <-> A. x ( x e. B -> A e. x ) ) )
8		df-int	|- |^| B = { z | A. x ( x e. B -> z e. x ) }
9	4 7 8	elab2gw	|- ( A e. _V -> ( A e. |^| B <-> A. x ( x e. B -> A e. x ) ) )
10	1 9	ax-mp	|- ( A e. |^| B <-> A. x ( x e. B -> A e. x ) )