This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem fvreseq0

Description: Equality of restricted functions is determined by their values (for functions with different domains). (Contributed by AV, 6-Jan-2019)

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

Proof

Step	Hyp	Ref	Expression
1		fnssres	\|- ( ( F Fn A /\ B C_ A ) -> ( F \|` B ) Fn B )
2		fnssres	\|- ( ( G Fn C /\ B C_ C ) -> ( G \|` B ) Fn B )
3		eqfnfv	\|- ( ( ( F \|` B ) Fn B /\ ( G \|` B ) Fn B ) -> ( ( F \|` B ) = ( G \|` B ) <-> A. x e. B ( ( F \|` B ) ` x ) = ( ( G \|` B ) ` x ) ) )
4		fvres	\|- ( x e. B -> ( ( F \|` B ) ` x ) = ( F ` x ) )
5		fvres	\|- ( x e. B -> ( ( G \|` B ) ` x ) = ( G ` x ) )
6	4 5	eqeq12d	\|- ( x e. B -> ( ( ( F \|` B ) ` x ) = ( ( G \|` B ) ` x ) <-> ( F ` x ) = ( G ` x ) ) )
7	6	ralbiia	\|- ( A. x e. B ( ( F \|` B ) ` x ) = ( ( G \|` B ) ` x ) <-> A. x e. B ( F ` x ) = ( G ` x ) )
8	3 7	bitrdi	\|- ( ( ( F \|` B ) Fn B /\ ( G \|` B ) Fn B ) -> ( ( F \|` B ) = ( G \|` B ) <-> A. x e. B ( F ` x ) = ( G ` x ) ) )
9	1 2 8	syl2an	\|- ( ( ( F Fn A /\ B C_ A ) /\ ( G Fn C /\ B C_ C ) ) -> ( ( F \|` B ) = ( G \|` B ) <-> A. x e. B ( F ` x ) = ( G ` x ) ) )
10	9	an4s	\|- ( ( ( F Fn A /\ G Fn C ) /\ ( B C_ A /\ B C_ C ) ) -> ( ( F \|` B ) = ( G \|` B ) <-> A. x e. B ( F ` x ) = ( G ` x ) ) )