Description: Technical lemma for bnj60 . This lemma may no longer be used or have become an indirect lemma of the theorem in question (i.e. a lemma of a lemma... of the theorem). (Contributed by Jonathan Ben-Naim, 3-Jun-2011) (New usage is discouraged.)
Ref | Expression | ||
---|---|---|---|
Hypotheses | bnj1234.2 | |
|
bnj1234.3 | |
||
bnj1234.4 | |
||
bnj1234.5 | |
||
Assertion | bnj1234 | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | bnj1234.2 | |
|
2 | bnj1234.3 | |
|
3 | bnj1234.4 | |
|
4 | bnj1234.5 | |
|
5 | fneq1 | |
|
6 | fveq1 | |
|
7 | reseq1 | |
|
8 | 7 | opeq2d | |
9 | 8 1 3 | 3eqtr4g | |
10 | 9 | fveq2d | |
11 | 6 10 | eqeq12d | |
12 | 11 | ralbidv | |
13 | 5 12 | anbi12d | |
14 | 13 | rexbidv | |
15 | 14 | cbvabv | |
16 | 15 2 4 | 3eqtr4i | |