Theorem bnj1536

Description: First-order logic and set theory. (Contributed by Jonathan Ben-Naim, 3-Jun-2011) (New usage is discouraged.)

	Ref	Expression
Hypotheses	bnj1536.1	|- ( ph -> F Fn A )
	bnj1536.2	|- ( ph -> G Fn A )
	bnj1536.3	|- ( ph -> B C_ A )
	bnj1536.4	|- ( ph -> A. x e. B ( F ` x ) = ( G ` x ) )
Assertion	bnj1536	|- ( ph -> ( F |` B ) = ( G |` B ) )

Proof

Step	Hyp	Ref	Expression
1		bnj1536.1	|- ( ph -> F Fn A )
2		bnj1536.2	|- ( ph -> G Fn A )
3		bnj1536.3	|- ( ph -> B C_ A )
4		bnj1536.4	|- ( ph -> A. x e. B ( F ` x ) = ( G ` x ) )
5		fvreseq	|- ( ( ( F Fn A /\ G Fn A ) /\ B C_ A ) -> ( ( F |` B ) = ( G |` B ) <-> A. x e. B ( F ` x ) = ( G ` x ) ) )
6	1 2 3 5	syl21anc	|- ( ph -> ( ( F |` B ) = ( G |` B ) <-> A. x e. B ( F ` x ) = ( G ` x ) ) )
7	4 6	mpbird	|- ( ph -> ( F |` B ) = ( G |` B ) )