Theorem wfr2aOLD

Description: Obsolete version of wfr2a as of 18-Nov-2024. (New usage is discouraged.) (Proof modification is discouraged.) (Contributed by Scott Fenton, 30-Jul-2020)

	Ref	Expression
Hypotheses	wfr2aOLD.1	|- R We A
	wfr2aOLD.2	|- R Se A
	wfr2aOLD.3	|- F = wrecs ( R , A , G )
Assertion	wfr2aOLD	|- ( X e. dom F -> ( F ` X ) = ( G ` ( F |` Pred ( R , A , X ) ) ) )

Proof

Step	Hyp	Ref	Expression
1		wfr2aOLD.1	|- R We A
2		wfr2aOLD.2	|- R Se A
3		wfr2aOLD.3	|- F = wrecs ( R , A , G )
4		fveq2	|- ( x = X -> ( F ` x ) = ( F ` X ) )
5		predeq3	|- ( x = X -> Pred ( R , A , x ) = Pred ( R , A , X ) )
6	5	reseq2d	|- ( x = X -> ( F |` Pred ( R , A , x ) ) = ( F |` Pred ( R , A , X ) ) )
7	6	fveq2d	|- ( x = X -> ( G ` ( F |` Pred ( R , A , x ) ) ) = ( G ` ( F |` Pred ( R , A , X ) ) ) )
8	4 7	eqeq12d	|- ( x = X -> ( ( F ` x ) = ( G ` ( F |` Pred ( R , A , x ) ) ) <-> ( F ` X ) = ( G ` ( F |` Pred ( R , A , X ) ) ) ) )
9	1 2 3	wfrlem12OLD	|- ( x e. dom F -> ( F ` x ) = ( G ` ( F |` Pred ( R , A , x ) ) ) )
10	8 9	vtoclga	|- ( X e. dom F -> ( F ` X ) = ( G ` ( F |` Pred ( R , A , X ) ) ) )