Metamath Proof Explorer
Description: Functionality of an operation defined on equivalence classes.
(Contributed by Jeff Madsen, 10-Jun-2010)
|
|
Ref |
Expression |
|
Hypotheses |
eropr2.1 |
|
|
|
eropr2.2 |
|
|
|
eropr2.3 |
|
|
|
eropr2.4 |
|
|
|
eropr2.5 |
|
|
|
eropr2.6 |
|
|
|
eropr2.7 |
|
|
Assertion |
eroprf2 |
|
Proof
Step |
Hyp |
Ref |
Expression |
1 |
|
eropr2.1 |
|
2 |
|
eropr2.2 |
|
3 |
|
eropr2.3 |
|
4 |
|
eropr2.4 |
|
5 |
|
eropr2.5 |
|
6 |
|
eropr2.6 |
|
7 |
|
eropr2.7 |
|
8 |
1 1 3 4 4 4 5 5 5 6 7 2 3 3 1
|
eroprf |
|