Theorem fresin

Description: An identity for the mapping relationship under restriction. (Contributed by Scott Fenton, 4-Sep-2011) (Proof shortened by Mario Carneiro, 26-May-2016)

	Ref	Expression
Assertion	fresin	⊢ ( 𝐹 : 𝐴 ⟶ 𝐵 → ( 𝐹 ↾ 𝑋 ) : ( 𝐴 ∩ 𝑋 ) ⟶ 𝐵 )

Proof

Step	Hyp	Ref	Expression
1		inss1	⊢ ( 𝐴 ∩ 𝑋 ) ⊆ 𝐴
2		fssres	⊢ ( ( 𝐹 : 𝐴 ⟶ 𝐵 ∧ ( 𝐴 ∩ 𝑋 ) ⊆ 𝐴 ) → ( 𝐹 ↾ ( 𝐴 ∩ 𝑋 ) ) : ( 𝐴 ∩ 𝑋 ) ⟶ 𝐵 )
3	1 2	mpan2	⊢ ( 𝐹 : 𝐴 ⟶ 𝐵 → ( 𝐹 ↾ ( 𝐴 ∩ 𝑋 ) ) : ( 𝐴 ∩ 𝑋 ) ⟶ 𝐵 )
4		resres	⊢ ( ( 𝐹 ↾ 𝐴 ) ↾ 𝑋 ) = ( 𝐹 ↾ ( 𝐴 ∩ 𝑋 ) )
5		ffn	⊢ ( 𝐹 : 𝐴 ⟶ 𝐵 → 𝐹 Fn 𝐴 )
6		fnresdm	⊢ ( 𝐹 Fn 𝐴 → ( 𝐹 ↾ 𝐴 ) = 𝐹 )
7	5 6	syl	⊢ ( 𝐹 : 𝐴 ⟶ 𝐵 → ( 𝐹 ↾ 𝐴 ) = 𝐹 )
8	7	reseq1d	⊢ ( 𝐹 : 𝐴 ⟶ 𝐵 → ( ( 𝐹 ↾ 𝐴 ) ↾ 𝑋 ) = ( 𝐹 ↾ 𝑋 ) )
9	4 8	eqtr3id	⊢ ( 𝐹 : 𝐴 ⟶ 𝐵 → ( 𝐹 ↾ ( 𝐴 ∩ 𝑋 ) ) = ( 𝐹 ↾ 𝑋 ) )
10	9	feq1d	⊢ ( 𝐹 : 𝐴 ⟶ 𝐵 → ( ( 𝐹 ↾ ( 𝐴 ∩ 𝑋 ) ) : ( 𝐴 ∩ 𝑋 ) ⟶ 𝐵 ↔ ( 𝐹 ↾ 𝑋 ) : ( 𝐴 ∩ 𝑋 ) ⟶ 𝐵 ) )
11	3 10	mpbid	⊢ ( 𝐹 : 𝐴 ⟶ 𝐵 → ( 𝐹 ↾ 𝑋 ) : ( 𝐴 ∩ 𝑋 ) ⟶ 𝐵 )