Metamath Proof Explorer
Description: Make a structure from a pair. (Contributed by Mario Carneiro, 29-Aug-2015)
|
|
Ref |
Expression |
|
Hypotheses |
strle1.i |
|
|
|
strle1.a |
|
|
|
strle2.j |
|
|
|
strle2.k |
|
|
|
strle2.b |
|
|
Assertion |
strle2 |
|
Proof
Step |
Hyp |
Ref |
Expression |
1 |
|
strle1.i |
|
2 |
|
strle1.a |
|
3 |
|
strle2.j |
|
4 |
|
strle2.k |
|
5 |
|
strle2.b |
|
6 |
|
df-pr |
|
7 |
1 2
|
strle1 |
|
8 |
4 5
|
strle1 |
|
9 |
7 8 3
|
strleun |
|
10 |
6 9
|
eqbrtri |
|