Theorem elint2

Description: Membership in class intersection. (Contributed by NM, 14-Oct-1999)

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

Proof

Step	Hyp	Ref	Expression
1		elint2.1	|- A e. _V
2	1	elint	|- ( A e. |^| B <-> A. x ( x e. B -> A e. x ) )
3		df-ral	|- ( A. x e. B A e. x <-> A. x ( x e. B -> A e. x ) )
4	2 3	bitr4i	|- ( A e. |^| B <-> A. x e. B A e. x )