Metamath Proof Explorer


Theorem fvpr1OLD

Description: Obsolete version of fvpr1 as of 26-Sep-2024. (Contributed by Jeff Madsen, 20-Jun-2010) (Proof modification is discouraged.) (New usage is discouraged.)

Ref Expression
Hypotheses fvpr1.1 AV
fvpr1.2 CV
Assertion fvpr1OLD ABACBDA=C

Proof

Step Hyp Ref Expression
1 fvpr1.1 AV
2 fvpr1.2 CV
3 df-pr ACBD=ACBD
4 3 fveq1i ACBDA=ACBDA
5 necom ABBA
6 fvunsn BAACBDA=ACA
7 5 6 sylbi ABACBDA=ACA
8 4 7 eqtrid ABACBDA=ACA
9 1 2 fvsn ACA=C
10 8 9 eqtrdi ABACBDA=C