Description: A fol lemma. See alequexv for a version with a disjoint variable condition requiring fewer axioms. Can be used to reduce the proof of spimt from 133 to 112 bytes. (Contributed by BJ, 6-Oct-2018)
| Ref | Expression | ||
|---|---|---|---|
| Assertion | bj-alequex | |- ( A. x ( x = y -> ph ) -> E. x ph ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | ax6e | |- E. x x = y |
|
| 2 | exim | |- ( A. x ( x = y -> ph ) -> ( E. x x = y -> E. x ph ) ) |
|
| 3 | 1 2 | mpi | |- ( A. x ( x = y -> ph ) -> E. x ph ) |