Metamath Proof Explorer


Theorem ov6g

Description: The value of an operation class abstraction. Special case. (Contributed by NM, 13-Nov-2006)

Ref Expression
Hypotheses ov6g.1 x y = A B R = S
ov6g.2 F = x y z | x y C z = R
Assertion ov6g A G B H A B C S J A F B = S

Proof

Step Hyp Ref Expression
1 ov6g.1 x y = A B R = S
2 ov6g.2 F = x y z | x y C z = R
3 df-ov A F B = F A B
4 eqid S = S
5 biidd x = A y = B S = S S = S
6 5 copsex2g A G B H x y A B = x y S = S S = S
7 4 6 mpbiri A G B H x y A B = x y S = S
8 7 3adant3 A G B H A B C x y A B = x y S = S
9 8 adantr A G B H A B C S J x y A B = x y S = S
10 eqeq1 w = A B w = x y A B = x y
11 10 anbi1d w = A B w = x y z = R A B = x y z = R
12 1 eqeq2d x y = A B z = R z = S
13 12 eqcoms A B = x y z = R z = S
14 13 pm5.32i A B = x y z = R A B = x y z = S
15 11 14 bitrdi w = A B w = x y z = R A B = x y z = S
16 15 2exbidv w = A B x y w = x y z = R x y A B = x y z = S
17 eqeq1 z = S z = S S = S
18 17 anbi2d z = S A B = x y z = S A B = x y S = S
19 18 2exbidv z = S x y A B = x y z = S x y A B = x y S = S
20 moeq * z z = R
21 20 mosubop * z x y w = x y z = R
22 21 a1i w C * z x y w = x y z = R
23 dfoprab2 x y z | x y C z = R = w z | x y w = x y x y C z = R
24 eleq1 w = x y w C x y C
25 24 anbi1d w = x y w C z = R x y C z = R
26 25 pm5.32i w = x y w C z = R w = x y x y C z = R
27 an12 w = x y w C z = R w C w = x y z = R
28 26 27 bitr3i w = x y x y C z = R w C w = x y z = R
29 28 2exbii x y w = x y x y C z = R x y w C w = x y z = R
30 19.42vv x y w C w = x y z = R w C x y w = x y z = R
31 29 30 bitri x y w = x y x y C z = R w C x y w = x y z = R
32 31 opabbii w z | x y w = x y x y C z = R = w z | w C x y w = x y z = R
33 2 23 32 3eqtri F = w z | w C x y w = x y z = R
34 16 19 22 33 fvopab3ig A B C S J x y A B = x y S = S F A B = S
35 34 3ad2antl3 A G B H A B C S J x y A B = x y S = S F A B = S
36 9 35 mpd A G B H A B C S J F A B = S
37 3 36 eqtrid A G B H A B C S J A F B = S