Intuitionistic Logic Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  ILE Home  >  Th. List  >  ov6g Unicode version

Theorem ov6g 5952
 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 5821 . 2
2 eqid 2157 . . . . . 6
3 biidd 171 . . . . . . 7
43copsex2g 4205 . . . . . 6
52, 4mpbiri 167 . . . . 5
653adant3 1002 . . . 4
8 eqeq1 2164 . . . . . . . 8
98anbi1d 461 . . . . . . 7
10 ov6g.1 . . . . . . . . . 10
1110eqeq2d 2169 . . . . . . . . 9
1211eqcoms 2160 . . . . . . . 8
1312pm5.32i 450 . . . . . . 7
149, 13bitrdi 195 . . . . . 6
15142exbidv 1848 . . . . 5
16 eqeq1 2164 . . . . . . 7
1716anbi2d 460 . . . . . 6
18172exbidv 1848 . . . . 5
19 moeq 2887 . . . . . . 7
2019mosubop 4649 . . . . . 6
2120a1i 9 . . . . 5
22 ov6g.2 . . . . . 6
23 dfoprab2 5862 . . . . . 6
24 eleq1 2220 . . . . . . . . . . . 12
2524anbi1d 461 . . . . . . . . . . 11
2625pm5.32i 450 . . . . . . . . . 10
27 an12 551 . . . . . . . . . 10
2826, 27bitr3i 185 . . . . . . . . 9
29282exbii 1586 . . . . . . . 8
30 19.42vv 1891 . . . . . . . 8
3129, 30bitri 183 . . . . . . 7
3231opabbii 4031 . . . . . 6
3322, 23, 323eqtri 2182 . . . . 5
3415, 18, 21, 33fvopab3ig 5539 . . . 4