Metamath Proof Explorer


Theorem ovelimab

Description: Operation value in an image. (Contributed by Mario Carneiro, 23-Dec-2013) (Revised by Mario Carneiro, 29-Jan-2014)

Ref Expression
Assertion ovelimab F Fn A B × C A D F B × C x B y C D = x F y

Proof

Step Hyp Ref Expression
1 fvelimab F Fn A B × C A D F B × C z B × C F z = D
2 fveq2 z = x y F z = F x y
3 df-ov x F y = F x y
4 2 3 eqtr4di z = x y F z = x F y
5 4 eqeq1d z = x y F z = D x F y = D
6 eqcom x F y = D D = x F y
7 5 6 bitrdi z = x y F z = D D = x F y
8 7 rexxp z B × C F z = D x B y C D = x F y
9 1 8 bitrdi F Fn A B × C A D F B × C x B y C D = x F y