Description: Obsolete version of opeq1 as of 25-May-2024. (Contributed by NM, 25-Jun-1998) (Revised by Mario Carneiro, 26-Apr-2015) (Proof modification is discouraged.) (New usage is discouraged.)
Ref | Expression | ||
---|---|---|---|
Assertion | opeq1OLD |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | eleq1 | ||
2 | 1 | anbi1d | |
3 | sneq | ||
4 | preq1 | ||
5 | 3 4 | preq12d | |
6 | 2 5 | ifbieq1d | |
7 | dfopif | ||
8 | dfopif | ||
9 | 6 7 8 | 3eqtr4g |