Description: Lemma for axcont . Eliminate the hypotheses from axcontlem10 . (Contributed by Scott Fenton, 20-Jun-2013)
Ref | Expression | ||
---|---|---|---|
Assertion | axcontlem11 | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | opeq2 | |
|
2 | 1 | breq2d | |
3 | breq1 | |
|
4 | 2 3 | orbi12d | |
5 | 4 | cbvrabv | |
6 | eqid | |
|
7 | 6 | axcontlem1 | |
8 | 5 7 | axcontlem10 | |