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 We A
	wfr2a.2	|- R Se A
	wfr2a.3	|- F = wrecs ( R , A , G )
Assertion	wfr2a	|- ( X e. dom F -> ( F ` X ) = ( G ` ( F |` Pred ( R , A , X ) ) ) )

Proof

Step	Hyp	Ref	Expression
1		wfr2a.1	|- R We A
2		wfr2a.2	|- R Se A
3		wfr2a.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	wfrlem12	|- ( 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 ) ) ) )