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	⊢ ( ( ( 𝑅 “ 𝐴 ) ⊆ 𝐴 ∧ 𝐵 ∈ 𝐴 ) → [ 𝐵 ] 𝑅 = [ 𝐵 ] ( 𝑅 ∩ ( 𝐴 × 𝐴 ) ) )

Proof

Step	Hyp	Ref	Expression
1		simpr	⊢ ( ( ( 𝑅 “ 𝐴 ) ⊆ 𝐴 ∧ 𝐵 ∈ 𝐴 ) → 𝐵 ∈ 𝐴 )
2	1	snssd	⊢ ( ( ( 𝑅 “ 𝐴 ) ⊆ 𝐴 ∧ 𝐵 ∈ 𝐴 ) → { 𝐵 } ⊆ 𝐴 )
3		df-ss	⊢ ( { 𝐵 } ⊆ 𝐴 ↔ ( { 𝐵 } ∩ 𝐴 ) = { 𝐵 } )
4	2 3	sylib	⊢ ( ( ( 𝑅 “ 𝐴 ) ⊆ 𝐴 ∧ 𝐵 ∈ 𝐴 ) → ( { 𝐵 } ∩ 𝐴 ) = { 𝐵 } )
5	4	imaeq2d	⊢ ( ( ( 𝑅 “ 𝐴 ) ⊆ 𝐴 ∧ 𝐵 ∈ 𝐴 ) → ( 𝑅 “ ( { 𝐵 } ∩ 𝐴 ) ) = ( 𝑅 “ { 𝐵 } ) )
6	5	ineq1d	⊢ ( ( ( 𝑅 “ 𝐴 ) ⊆ 𝐴 ∧ 𝐵 ∈ 𝐴 ) → ( ( 𝑅 “ ( { 𝐵 } ∩ 𝐴 ) ) ∩ 𝐴 ) = ( ( 𝑅 “ { 𝐵 } ) ∩ 𝐴 ) )
7		imass2	⊢ ( { 𝐵 } ⊆ 𝐴 → ( 𝑅 “ { 𝐵 } ) ⊆ ( 𝑅 “ 𝐴 ) )
8	2 7	syl	⊢ ( ( ( 𝑅 “ 𝐴 ) ⊆ 𝐴 ∧ 𝐵 ∈ 𝐴 ) → ( 𝑅 “ { 𝐵 } ) ⊆ ( 𝑅 “ 𝐴 ) )
9		simpl	⊢ ( ( ( 𝑅 “ 𝐴 ) ⊆ 𝐴 ∧ 𝐵 ∈ 𝐴 ) → ( 𝑅 “ 𝐴 ) ⊆ 𝐴 )
10	8 9	sstrd	⊢ ( ( ( 𝑅 “ 𝐴 ) ⊆ 𝐴 ∧ 𝐵 ∈ 𝐴 ) → ( 𝑅 “ { 𝐵 } ) ⊆ 𝐴 )
11		df-ss	⊢ ( ( 𝑅 “ { 𝐵 } ) ⊆ 𝐴 ↔ ( ( 𝑅 “ { 𝐵 } ) ∩ 𝐴 ) = ( 𝑅 “ { 𝐵 } ) )
12	10 11	sylib	⊢ ( ( ( 𝑅 “ 𝐴 ) ⊆ 𝐴 ∧ 𝐵 ∈ 𝐴 ) → ( ( 𝑅 “ { 𝐵 } ) ∩ 𝐴 ) = ( 𝑅 “ { 𝐵 } ) )
13	6 12	eqtr2d	⊢ ( ( ( 𝑅 “ 𝐴 ) ⊆ 𝐴 ∧ 𝐵 ∈ 𝐴 ) → ( 𝑅 “ { 𝐵 } ) = ( ( 𝑅 “ ( { 𝐵 } ∩ 𝐴 ) ) ∩ 𝐴 ) )
14		imainrect	⊢ ( ( 𝑅 ∩ ( 𝐴 × 𝐴 ) ) “ { 𝐵 } ) = ( ( 𝑅 “ ( { 𝐵 } ∩ 𝐴 ) ) ∩ 𝐴 )
15	13 14	eqtr4di	⊢ ( ( ( 𝑅 “ 𝐴 ) ⊆ 𝐴 ∧ 𝐵 ∈ 𝐴 ) → ( 𝑅 “ { 𝐵 } ) = ( ( 𝑅 ∩ ( 𝐴 × 𝐴 ) ) “ { 𝐵 } ) )
16		df-ec	⊢ [ 𝐵 ] 𝑅 = ( 𝑅 “ { 𝐵 } )
17		df-ec	⊢ [ 𝐵 ] ( 𝑅 ∩ ( 𝐴 × 𝐴 ) ) = ( ( 𝑅 ∩ ( 𝐴 × 𝐴 ) ) “ { 𝐵 } )
18	15 16 17	3eqtr4g	⊢ ( ( ( 𝑅 “ 𝐴 ) ⊆ 𝐴 ∧ 𝐵 ∈ 𝐴 ) → [ 𝐵 ] 𝑅 = [ 𝐵 ] ( 𝑅 ∩ ( 𝐴 × 𝐴 ) ) )