New Foundations Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  NFE Home  >  Th. List  >  ov6g Unicode version

Theorem ov6g 5600
 Description: The value of an operation class abstraction. Special case. (Contributed by set.mm contributors, 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 5526 . 2
2 eqid 2353 . . . . . 6
3 biidd 228 . . . . . . 7
43copsex2g 4609 . . . . . 6
52, 4mpbiri 224 . . . . 5
653adant3 975 . . . 4
8 eqeq1 2359 . . . . . . . 8
98anbi1d 685 . . . . . . 7
10 ov6g.1 . . . . . . . . . 10
1110eqeq2d 2364 . . . . . . . . 9
1211eqcoms 2356 . . . . . . . 8
1312pm5.32i 618 . . . . . . 7
149, 13syl6bb 252 . . . . . 6
15142exbidv 1628 . . . . 5
16 eqeq1 2359 . . . . . . 7
1716anbi2d 684 . . . . . 6
18172exbidv 1628 . . . . 5
19 moeq 3012 . . . . . . 7
2019mosubop 4613 . . . . . 6
2120a1i 10 . . . . 5
22 ov6g.2 . . . . . 6
23 dfoprab2 5558 . . . . . 6
24 eleq1 2413 . . . . . . . . . . . 12
2524anbi1d 685 . . . . . . . . . . 11
2625pm5.32i 618 . . . . . . . . . 10
27 an12 772 . . . . . . . . . 10
2826, 27bitr3i 242 . . . . . . . . 9
29282exbii 1583 . . . . . . . 8
30 19.42vv 1907 . . . . . . . 8
3129, 30bitri 240 . . . . . . 7
3231opabbii 4626 . . . . . 6
3322, 23, 323eqtri 2377 . . . . 5
3415, 18, 21, 33fvopab3ig 5387 . . . 4