Description: Proof of ax6e (hence ax6 ) from Tarski's system, ax-c9 , ax-c16 . Remark: ax-6 is used only via its principal (unbundled) instance ax6v . (Contributed by BJ, 22-Dec-2020) (Proof modification is discouraged.) (New usage is discouraged.)
| Ref | Expression | ||
|---|---|---|---|
| Assertion | bj-ax6e | |- E. x x = y |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | 19.2 | |- ( A. x x = y -> E. x x = y ) |
|
| 2 | 1 | a1d | |- ( A. x x = y -> ( y = z -> E. x x = y ) ) |
| 3 | bj-ax6elem1 | |- ( -. A. x x = y -> ( y = z -> A. x y = z ) ) |
|
| 4 | bj-ax6elem2 | |- ( A. x y = z -> E. x x = y ) |
|
| 5 | 3 4 | syl6 | |- ( -. A. x x = y -> ( y = z -> E. x x = y ) ) |
| 6 | 2 5 | pm2.61i | |- ( y = z -> E. x x = y ) |
| 7 | ax6evr | |- E. z y = z |
|
| 8 | 6 7 | exlimiiv | |- E. x x = y |