Description: An equivalent expression for universal quantification over a non-occurring variable proved over ax-1 -- ax-5 . The forward implication can be strengthened when ax-6 is posited (which implies that models are non-empty), see spvw . The reverse implication can be seen as a strengthening of ax-5 (since the antecedent of the implication is weakened). See bj-exextruan for a dual statement.
An approximate meaning is: the universal quantification of a proposition over a non-occurring variable holds if and only if the proposition holds in nonempty universes. (Contributed by BJ, 14-Mar-2026) (Proof modification is discouraged.)
| Ref | Expression | ||
|---|---|---|---|
| Assertion | bj-alextruim | |- ( A. x ph <-> ( E. x T. -> ph ) ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | bj-spvw | |- ( E. x T. -> ( ph <-> A. x ph ) ) |
|
| 2 | 1 | biimprcd | |- ( A. x ph -> ( E. x T. -> ph ) ) |
| 3 | ax-5 | |- ( ph -> A. x ph ) |
|
| 4 | 3 | imim2i | |- ( ( E. x T. -> ph ) -> ( E. x T. -> A. x ph ) ) |
| 5 | 19.38 | |- ( ( E. x T. -> A. x ph ) -> A. x ( T. -> ph ) ) |
|
| 6 | pm2.27 | |- ( T. -> ( ( T. -> ph ) -> ph ) ) |
|
| 7 | 6 | mptru | |- ( ( T. -> ph ) -> ph ) |
| 8 | 5 7 | sylg | |- ( ( E. x T. -> A. x ph ) -> A. x ph ) |
| 9 | 4 8 | syl | |- ( ( E. x T. -> ph ) -> A. x ph ) |
| 10 | 2 9 | impbii | |- ( A. x ph <-> ( E. x T. -> ph ) ) |