Theorem tfr2a

Description: A weak version of tfr2 which is useful for proofs that avoid the Axiom of Replacement. (Contributed by Mario Carneiro, 24-Jun-2015)

	Ref	Expression
Hypothesis	tfr.1	|- F = recs ( G )
Assertion	tfr2a	|- ( A e. dom F -> ( F ` A ) = ( G ` ( F |` A ) ) )

Proof

Step	Hyp	Ref	Expression
1		tfr.1	|- F = recs ( G )
2		eqid	|- { f | E. x e. On ( f Fn x /\ A. y e. x ( f ` y ) = ( G ` ( f |` y ) ) ) } = { f | E. x e. On ( f Fn x /\ A. y e. x ( f ` y ) = ( G ` ( f |` y ) ) ) }
3	2	tfrlem9	|- ( A e. dom recs ( G ) -> ( recs ( G ) ` A ) = ( G ` ( recs ( G ) |` A ) ) )
4	1	dmeqi	|- dom F = dom recs ( G )
5	3 4	eleq2s	|- ( A e. dom F -> ( recs ( G ) ` A ) = ( G ` ( recs ( G ) |` A ) ) )
6	1	fveq1i	|- ( F ` A ) = ( recs ( G ) ` A )
7	1	reseq1i	|- ( F |` A ) = ( recs ( G ) |` A )
8	7	fveq2i	|- ( G ` ( F |` A ) ) = ( G ` ( recs ( G ) |` A ) )
9	5 6 8	3eqtr4g	|- ( A e. dom F -> ( F ` A ) = ( G ` ( F |` A ) ) )