Description: An equivalent expression for existential quantification over a non-occurring variable proved over ax-1 -- ax-5 . The forward implication can be seen as a strengthening of ax-5 (a conjunct is added to the consequent of the implication). The reverse implication can be strengthened when ax-6 is posited (which implies that models are non-empty), see 19.8v . See bj-alextruim for a dual statement.
An approximate meaning is: the existential quantification of a proposition over a non-occurring variable holds if and only if the proposition holds and the universe is nonempty. (Contributed by BJ, 14-Mar-2026) (Proof modification is discouraged.)
| Ref | Expression | ||
|---|---|---|---|
| Assertion | bj-exextruan | |- ( E. x ph <-> ( E. x T. /\ ph ) ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | trud | |- ( ph -> T. ) |
|
| 2 | 1 | eximi | |- ( E. x ph -> E. x T. ) |
| 3 | ax5e | |- ( E. x ph -> ph ) |
|
| 4 | 2 3 | jca | |- ( E. x ph -> ( E. x T. /\ ph ) ) |
| 5 | bj-spvew | |- ( E. x T. -> ( ph <-> E. x ph ) ) |
|
| 6 | 5 | biimpa | |- ( ( E. x T. /\ ph ) -> E. x ph ) |
| 7 | 4 6 | impbii | |- ( E. x ph <-> ( E. x T. /\ ph ) ) |