Theorem wfr2a

Description: A weak version of wfr2 which is useful for proofs that avoid the Axiom of Replacement. (Contributed by Scott Fenton, 30-Jul-2020)

	Ref	Expression
Hypotheses	wfr2a.1	$$⊢R\mathrm{We}A$$
	wfr2a.2	$$⊢R\mathrm{Se}A$$
	wfr2a.3	$$⊢F=\mathrm{wrecs}\left(R,A,G\right)$$
Assertion	wfr2a	$$⊢X\in \mathrm{dom}F\to F\left(X\right)=G\left({F\upharpoonright }_{Pred\left(R,A,X\right)}\right)$$

Proof

Step	Hyp	Ref	Expression
1		wfr2a.1	$$⊢R\mathrm{We}A$$
2		wfr2a.2	$$⊢R\mathrm{Se}A$$
3		wfr2a.3	$$⊢F=\mathrm{wrecs}\left(R,A,G\right)$$
4		fveq2	$$⊢x=X\to F\left(x\right)=F\left(X\right)$$
5		predeq3	$$⊢x=X\to Pred\left(R,A,x\right)=Pred\left(R,A,X\right)$$
6	5	reseq2d	$$⊢x=X\to {F\upharpoonright }_{Pred\left(R,A,x\right)}={F\upharpoonright }_{Pred\left(R,A,X\right)}$$
7	6	fveq2d	$$⊢x=X\to G\left({F\upharpoonright }_{Pred\left(R,A,x\right)}\right)=G\left({F\upharpoonright }_{Pred\left(R,A,X\right)}\right)$$
8	4 7	eqeq12d	$$⊢x=X\to \left(F\left(x\right)=G\left({F\upharpoonright }_{Pred\left(R,A,x\right)}\right)\leftrightarrow F\left(X\right)=G\left({F\upharpoonright }_{Pred\left(R,A,X\right)}\right)\right)$$
9	1 2 3	wfrlem12	$$⊢x\in \mathrm{dom}F\to F\left(x\right)=G\left({F\upharpoonright }_{Pred\left(R,A,x\right)}\right)$$
10	8 9	vtoclga	$$⊢X\in \mathrm{dom}F\to F\left(X\right)=G\left({F\upharpoonright }_{Pred\left(R,A,X\right)}\right)$$