Theorem elecres

Description: Elementhood in the restricted coset of B . (Contributed by Peter Mazsa, 21-Sep-2018)

	Ref	Expression
Assertion	elecres	|- ( C e. V -> ( C e. [ B ] ( R |` A ) <-> ( B e. A /\ B R C ) ) )

Proof

Step	Hyp	Ref	Expression
1		relres	|- Rel ( R |` A )
2		relelec	|- ( Rel ( R |` A ) -> ( C e. [ B ] ( R |` A ) <-> B ( R |` A ) C ) )
3	1 2	ax-mp	|- ( C e. [ B ] ( R |` A ) <-> B ( R |` A ) C )
4		brres	|- ( C e. V -> ( B ( R |` A ) C <-> ( B e. A /\ B R C ) ) )
5	3 4	bitrid	|- ( C e. V -> ( C e. [ B ] ( R |` A ) <-> ( B e. A /\ B R C ) ) )