Metamath Proof Explorer


Theorem wfr2OLD

Description: Obsolete proof of wfr2 as of 18-Nov-2024. (New usage is discouraged.) (Proof modification is discouraged.) (Contributed by Scott Fenton, 18-Apr-2011) (Revised by Mario Carneiro, 26-Jun-2015)

Ref Expression
Hypotheses wfr2OLD.1 R We A
wfr2OLD.2 R Se A
wfr2OLD.3 F = wrecs R A G
Assertion wfr2OLD X A F X = G F Pred R A X

Proof

Step Hyp Ref Expression
1 wfr2OLD.1 R We A
2 wfr2OLD.2 R Se A
3 wfr2OLD.3 F = wrecs R A G
4 eqid F x G F Pred R A x = F x G F Pred R A x
5 1 2 3 4 wfrlem16OLD dom F = A
6 5 eleq2i X dom F X A
7 1 2 3 wfr2aOLD X dom F F X = G F Pred R A X
8 6 7 sylbir X A F X = G F Pred R A X