Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > ax13lem1 | Structured version Visualization version Unicode version |
Description: A version of ax13v 2247 with one distinct variable restriction dropped. For convenience, is kept on the right side of equations. The proof of ax13 2249 bases on ideas from NM, 24-Dec-2015. (Contributed by Wolf Lammen, 8-Sep-2018.) (New usage is discouraged.) |
Ref | Expression |
---|---|
ax13lem1 |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | equviniva 1960 | . 2 | |
2 | ax13v 2247 | . . . . 5 | |
3 | equeucl 1951 | . . . . . 6 | |
4 | 3 | alimdv 1845 | . . . . 5 |
5 | 2, 4 | syl9 77 | . . . 4 |
6 | 5 | impd 447 | . . 3 |
7 | 6 | exlimdv 1861 | . 2 |
8 | 1, 7 | syl5 34 | 1 |
Colors of variables: wff setvar class |
Syntax hints: wn 3 wi 4 wa 384 wal 1481 wex 1704 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1722 ax-4 1737 ax-5 1839 ax-6 1888 ax-7 1935 ax-13 2246 |
This theorem depends on definitions: df-bi 197 df-an 386 df-ex 1705 |
This theorem is referenced by: ax13 2249 ax6e 2250 ax13lem2 2296 nfeqf2 2297 wl-19.8eqv 33309 wl-19.2reqv 33310 wl-dveeq12 33311 |
Copyright terms: Public domain | W3C validator |