Metamath Proof Explorer

Theorem fvreseq

Description: Equality of restricted functions is determined by their values. (Contributed by NM, 3-Aug-1994) (Proof shortened by AV, 4-Mar-2019)

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

Step	Hyp	Ref	Expression
1		fvreseq0	\|- ( ( ( F Fn A /\ G Fn A ) /\ ( B C_ A /\ B C_ A ) ) -> ( ( F \|` B ) = ( G \|` B ) <-> A. x e. B ( F ` x ) = ( G ` x ) ) )
2	1	anabsan2	\|- ( ( ( F Fn A /\ G Fn A ) /\ B C_ A ) -> ( ( F \|` B ) = ( G \|` B ) <-> A. x e. B ( F ` x ) = ( G ` x ) ) )

Step

Hyp

Ref

Expression

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

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