Metamath Proof Explorer

Theorem fvreseq1

Description: Equality of a function restricted to the domain of another function. (Contributed by AV, 6-Jan-2019)

Ref Expression
Assertion fvreseq1 
|- ( ( ( F Fn A /\ G Fn B ) /\ B C_ A ) -> ( ( F |` B ) = G <-> A. x e. B ( F ` x ) = ( G ` x ) ) )

Proof

Step Hyp Ref Expression
1 fnresdm 
 |-  ( G Fn B -> ( G |` B ) = G )
2 1 ad2antlr 
 |-  ( ( ( F Fn A /\ G Fn B ) /\ B C_ A ) -> ( G |` B ) = G )
3 2 eqcomd 
 |-  ( ( ( F Fn A /\ G Fn B ) /\ B C_ A ) -> G = ( G |` B ) )
4 3 eqeq2d 
 |-  ( ( ( F Fn A /\ G Fn B ) /\ B C_ A ) -> ( ( F |` B ) = G <-> ( F |` B ) = ( G |` B ) ) )
5 ssid 
 |-  B C_ B
6 fvreseq0 
 |-  ( ( ( F Fn A /\ G Fn B ) /\ ( B C_ A /\ B C_ B ) ) -> ( ( F |` B ) = ( G |` B ) <-> A. x e. B ( F ` x ) = ( G ` x ) ) )
7 5 6 mpanr2 
 |-  ( ( ( F Fn A /\ G Fn B ) /\ B C_ A ) -> ( ( F |` B ) = ( G |` B ) <-> A. x e. B ( F ` x ) = ( G ` x ) ) )
8 4 7 bitrd 
 |-  ( ( ( F Fn A /\ G Fn B ) /\ B C_ A ) -> ( ( F |` B ) = G <-> A. x e. B ( F ` x ) = ( G ` x ) ) )