Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  ov6g Structured version   Unicode version

Theorem ov6g 6203
 Description: The value of an operation class abstraction. Special case. (Contributed by NM, 13-Nov-2006.)
Hypotheses
Ref Expression
ov6g.1
ov6g.2
Assertion
Ref Expression
ov6g
Distinct variable groups:   ,,,   ,,,   ,,,   ,   ,,,
Allowed substitution hints:   (,)   (,,)   (,,)   (,,)   (,,)

Proof of Theorem ov6g
Dummy variable is distinct from all other variables.
StepHypRef Expression
1 df-ov 6076 . 2
2 eqid 2435 . . . . . 6
3 biidd 229 . . . . . . 7
43copsex2g 4436 . . . . . 6
52, 4mpbiri 225 . . . . 5
653adant3 977 . . . 4
8 eqeq1 2441 . . . . . . . 8
98anbi1d 686 . . . . . . 7
10 ov6g.1 . . . . . . . . . 10
1110eqeq2d 2446 . . . . . . . . 9
1211eqcoms 2438 . . . . . . . 8
1312pm5.32i 619 . . . . . . 7
149, 13syl6bb 253 . . . . . 6
15142exbidv 1638 . . . . 5
16 eqeq1 2441 . . . . . . 7
1716anbi2d 685 . . . . . 6
18172exbidv 1638 . . . . 5
19 moeq 3102 . . . . . . 7
2019mosubop 4447 . . . . . 6
2120a1i 11 . . . . 5
22 ov6g.2 . . . . . 6
23 dfoprab2 6113 . . . . . 6
24 eleq1 2495 . . . . . . . . . . . 12
2524anbi1d 686 . . . . . . . . . . 11
2625pm5.32i 619 . . . . . . . . . 10
27 an12 773 . . . . . . . . . 10
2826, 27bitr3i 243 . . . . . . . . 9
29282exbii 1593 . . . . . . . 8
30 19.42vv 1930 . . . . . . . 8
3129, 30bitri 241 . . . . . . 7
3231opabbii 4264 . . . . . 6
3322, 23, 323eqtri 2459 . . . . 5
3415, 18, 21, 33fvopab3ig 5795 . . . 4