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=\mathrm{recs}\left(G\right)$$
Assertion	tfr2a	$$⊢A\in \mathrm{dom}F\to F\left(A\right)=G\left({F\upharpoonright }_A\right)$$

Proof

Step	Hyp	Ref	Expression
1		tfr.1	$$⊢F=\mathrm{recs}\left(G\right)$$
2		eqid	$$⊢\left\{f|\exists x\in \mathrm{On}\left(fFnx\wedge \forall y\in xf\left(y\right)=G\left({f\upharpoonright }_y\right)\right)\right\}=\left\{f|\exists x\in \mathrm{On}\left(fFnx\wedge \forall y\in xf\left(y\right)=G\left({f\upharpoonright }_y\right)\right)\right\}$$
3	2	tfrlem9	$$⊢A\in \mathrm{dom}\mathrm{recs}\left(G\right)\to \mathrm{recs}\left(G\right)\left(A\right)=G\left({\mathrm{recs}\left(G\right)\upharpoonright }_A\right)$$
4	1	dmeqi	$$⊢\mathrm{dom}F=\mathrm{dom}\mathrm{recs}\left(G\right)$$
5	3 4	eleq2s	$$⊢A\in \mathrm{dom}F\to \mathrm{recs}\left(G\right)\left(A\right)=G\left({\mathrm{recs}\left(G\right)\upharpoonright }_A\right)$$
6	1	fveq1i	$$⊢F\left(A\right)=\mathrm{recs}\left(G\right)\left(A\right)$$
7	1	reseq1i	$$⊢{F\upharpoonright }_A={\mathrm{recs}\left(G\right)\upharpoonright }_A$$
8	7	fveq2i	$$⊢G\left({F\upharpoonright }_A\right)=G\left({\mathrm{recs}\left(G\right)\upharpoonright }_A\right)$$
9	5 6 8	3eqtr4g	$$⊢A\in \mathrm{dom}F\to F\left(A\right)=G\left({F\upharpoonright }_A\right)$$