Metamath Proof Explorer


Theorem fvpr2gOLD

Description: Obsolete version of fvpr2g as of 26-Sep-2024. (Contributed by Alexander van der Vekens, 3-Dec-2017) (Proof modification is discouraged.) (New usage is discouraged.)

Ref Expression
Assertion fvpr2gOLD B V D W A B A C B D B = D

Proof

Step Hyp Ref Expression
1 prcom A C B D = B D A C
2 df-pr B D A C = B D A C
3 1 2 eqtri A C B D = B D A C
4 3 fveq1i A C B D B = B D A C B
5 fvunsn A B B D A C B = B D B
6 4 5 syl5eq A B A C B D B = B D B
7 6 3ad2ant3 B V D W A B A C B D B = B D B
8 fvsng B V D W B D B = D
9 8 3adant3 B V D W A B B D B = D
10 7 9 eqtrd B V D W A B A C B D B = D