Metamath Proof Explorer


Theorem fun2ssres

Description: Equality of restrictions of a function and a subclass. (Contributed by NM, 16-Aug-1994)

Ref Expression
Assertion fun2ssres ( ( Fun 𝐹𝐺𝐹𝐴 ⊆ dom 𝐺 ) → ( 𝐹𝐴 ) = ( 𝐺𝐴 ) )

Proof

Step Hyp Ref Expression
1 resabs1 ( 𝐴 ⊆ dom 𝐺 → ( ( 𝐹 ↾ dom 𝐺 ) ↾ 𝐴 ) = ( 𝐹𝐴 ) )
2 1 eqcomd ( 𝐴 ⊆ dom 𝐺 → ( 𝐹𝐴 ) = ( ( 𝐹 ↾ dom 𝐺 ) ↾ 𝐴 ) )
3 funssres ( ( Fun 𝐹𝐺𝐹 ) → ( 𝐹 ↾ dom 𝐺 ) = 𝐺 )
4 3 reseq1d ( ( Fun 𝐹𝐺𝐹 ) → ( ( 𝐹 ↾ dom 𝐺 ) ↾ 𝐴 ) = ( 𝐺𝐴 ) )
5 2 4 sylan9eqr ( ( ( Fun 𝐹𝐺𝐹 ) ∧ 𝐴 ⊆ dom 𝐺 ) → ( 𝐹𝐴 ) = ( 𝐺𝐴 ) )
6 5 3impa ( ( Fun 𝐹𝐺𝐹𝐴 ⊆ dom 𝐺 ) → ( 𝐹𝐴 ) = ( 𝐺𝐴 ) )