This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 dfss2 
 |-  ( { 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 dfss2 
 |-  ( ( 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 ) ) )