Theorem ecinxp

Description: Restrict the relation in an equivalence class to a base set. (Contributed by Mario Carneiro, 10-Jul-2015)

	Ref	Expression
Assertion	ecinxp	|- ( ( ( R " A ) C_ A /\ B e. A ) -> [ B ] R = [ B ] ( R i^i ( A X. A ) ) )

Proof

Step	Hyp	Ref	Expression
1		simpr	|- ( ( ( R " A ) C_ A /\ B e. A ) -> B e. A )
2	1	snssd	|- ( ( ( R " A ) C_ A /\ B e. A ) -> { B } C_ A )
3		df-ss	|- ( { B } C_ A <-> ( { B } i^i A ) = { B } )
4	2 3	sylib	|- ( ( ( R " A ) C_ A /\ B e. A ) -> ( { B } i^i A ) = { B } )
5	4	imaeq2d	|- ( ( ( R " A ) C_ A /\ B e. A ) -> ( R " ( { B } i^i A ) ) = ( R " { B } ) )
6	5	ineq1d	|- ( ( ( R " A ) C_ A /\ B e. A ) -> ( ( R " ( { B } i^i A ) ) i^i A ) = ( ( R " { B } ) i^i A ) )
7		imass2	|- ( { B } C_ A -> ( R " { B } ) C_ ( R " A ) )
8	2 7	syl	|- ( ( ( R " A ) C_ A /\ B e. A ) -> ( R " { B } ) C_ ( R " A ) )
9		simpl	|- ( ( ( R " A ) C_ A /\ B e. A ) -> ( R " A ) C_ A )
10	8 9	sstrd	|- ( ( ( R " A ) C_ A /\ B e. A ) -> ( R " { B } ) C_ A )
11		df-ss	|- ( ( R " { B } ) C_ A <-> ( ( R " { B } ) i^i A ) = ( R " { B } ) )
12	10 11	sylib	|- ( ( ( R " A ) C_ A /\ B e. A ) -> ( ( R " { B } ) i^i A ) = ( R " { B } ) )
13	6 12	eqtr2d	|- ( ( ( R " A ) C_ A /\ B e. A ) -> ( R " { B } ) = ( ( R " ( { B } i^i A ) ) i^i A ) )
14		imainrect	|- ( ( R i^i ( A X. A ) ) " { B } ) = ( ( R " ( { B } i^i A ) ) i^i A )
15	13 14	eqtr4di	|- ( ( ( R " A ) C_ A /\ B e. A ) -> ( R " { B } ) = ( ( R i^i ( A X. A ) ) " { B } ) )
16		df-ec	|- [ B ] R = ( R " { B } )
17		df-ec	|- [ B ] ( R i^i ( A X. A ) ) = ( ( R i^i ( A X. A ) ) " { B } )
18	15 16 17	3eqtr4g	|- ( ( ( R " A ) C_ A /\ B e. A ) -> [ B ] R = [ B ] ( R i^i ( A X. A ) ) )