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

Metamath Proof Explorer

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 ) ) )