Theorem elriin

Description: Elementhood in a relative intersection. (Contributed by Mario Carneiro, 30-Dec-2016)

	Ref	Expression
Assertion	elriin	|- ( B e. ( A i^i |^|_ x e. X S ) <-> ( B e. A /\ A. x e. X B e. S ) )

Proof

Step	Hyp	Ref	Expression
1		elin	|- ( B e. ( A i^i |^|_ x e. X S ) <-> ( B e. A /\ B e. |^|_ x e. X S ) )
2		eliin	|- ( B e. A -> ( B e. |^|_ x e. X S <-> A. x e. X B e. S ) )
3	2	pm5.32i	|- ( ( B e. A /\ B e. |^|_ x e. X S ) <-> ( B e. A /\ A. x e. X B e. S ) )
4	1 3	bitri	|- ( B e. ( A i^i |^|_ x e. X S ) <-> ( B e. A /\ A. x e. X B e. S ) )