Description: Lemma for nfeqf2 . This lemma is equivalent to ax13v with one distinct variable constraint removed. (Contributed by Wolf Lammen, 8-Sep-2018) Reduce axiom usage. (Revised by Wolf Lammen, 18-Oct-2020) (New usage is discouraged.)
Ref | Expression | ||
---|---|---|---|
Assertion | ax13lem2 | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | ax13lem1 | |
|
2 | equeucl | |
|
3 | 2 | eximi | |
4 | 19.36v | |
|
5 | 3 4 | sylib | |
6 | 1 5 | syl9 | |
7 | 6 | alrimdv | |
8 | equequ2 | |
|
9 | 8 | equsalvw | |
10 | 7 9 | imbitrdi | |