Metamath Proof Explorer


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 F : A B F X : A X B

Proof

Step Hyp Ref Expression
1 inss1 A X A
2 fssres F : A B A X A F A X : A X B
3 1 2 mpan2 F : A B F A X : A X B
4 resres F A X = F A X
5 ffn F : A B F Fn A
6 fnresdm F Fn A F A = F
7 5 6 syl F : A B F A = F
8 7 reseq1d F : A B F A X = F X
9 4 8 eqtr3id F : A B F A X = F X
10 9 feq1d F : A B F A X : A X B F X : A X B
11 3 10 mpbid F : A B F X : A X B