Description: Alternate proof of axc10 . Shorter. One can prove a version with DV ( x , y ) without ax-13 , by using ax6ev instead of ax6e . (Contributed by BJ, 31-Mar-2021) (Proof modification is discouraged.)
| Ref | Expression | ||
|---|---|---|---|
| Assertion | bj-axc10 | |- ( A. x ( x = y -> A. x ph ) -> ph ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | ax6e | |- E. x x = y |
|
| 2 | exim | |- ( A. x ( x = y -> A. x ph ) -> ( E. x x = y -> E. x A. x ph ) ) |
|
| 3 | 1 2 | mpi | |- ( A. x ( x = y -> A. x ph ) -> E. x A. x ph ) |
| 4 | axc7e | |- ( E. x A. x ph -> ph ) |
|
| 5 | 3 4 | syl | |- ( A. x ( x = y -> A. x ph ) -> ph ) |