Description: Lemma for axcont . State the defining properties of the value of F . (Contributed by Scott Fenton, 19-Jun-2013)
Ref | Expression | ||
---|---|---|---|
Hypotheses | axcontlem5.1 | |
|
axcontlem5.2 | |
||
Assertion | axcontlem6 | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | axcontlem5.1 | |
|
2 | axcontlem5.2 | |
|
3 | eqid | |
|
4 | 2 | axcontlem1 | |
5 | 1 4 | axcontlem5 | |
6 | 3 5 | mpbii | |
7 | fveq2 | |
|
8 | fveq2 | |
|
9 | 8 | oveq2d | |
10 | fveq2 | |
|
11 | 10 | oveq2d | |
12 | 9 11 | oveq12d | |
13 | 7 12 | eqeq12d | |
14 | 13 | cbvralvw | |
15 | 14 | anbi2i | |
16 | 6 15 | sylib | |