Mathbox for BJ |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > Mathboxes > bj-substax12 | Structured version Visualization version GIF version |
Description: Equivalent form of the
axiom of substitution bj-ax12 34524. Although both
sides need a DV condition on 𝑥, 𝑡 (or as in bj-ax12v3 34553 on
𝑡,
𝜑) to hold, their
equivalence holds without DV conditions. The
forward implication is proved in modal (K4) while the reverse implication
is proved in modal (T5). The LHS has the advantage of not involving
nested quantifiers on the same variable. Its metaweakening is proved from
the core axiom schemes in bj-substw 34590. Note that in the LHS, the reverse
implication holds by equs4 2415 (or equs4v 2009 if a DV condition is added on
𝑥,
𝑡 as in bj-ax12 34524).
The LHS can be read as saying that if there exists a setvar equal to a given term witnessing 𝜑, then all setvars equal to that term also witness 𝜑. An equivalent suggestive form for the LHS is ¬ (∃𝑥(𝑥 = 𝑡 ∧ 𝜑) ∧ ∃𝑥(𝑥 = 𝑡 ∧ ¬ 𝜑)), which expresses that there can be no two variables both equal to a given term, one witnessing 𝜑 and the other witnessing ¬ 𝜑. (Contributed by BJ, 21-May-2024.) (Proof modification is discouraged.) |
Ref | Expression |
---|---|
bj-substax12 | ⊢ ((∃𝑥(𝑥 = 𝑡 ∧ 𝜑) → ∀𝑥(𝑥 = 𝑡 → 𝜑)) ↔ ∀𝑥(𝑥 = 𝑡 → (𝜑 → ∀𝑥(𝑥 = 𝑡 → 𝜑)))) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | bj-modal4 34582 | . . . . 5 ⊢ (∀𝑥(𝑥 = 𝑡 → 𝜑) → ∀𝑥∀𝑥(𝑥 = 𝑡 → 𝜑)) | |
2 | 1 | imim2i 16 | . . . 4 ⊢ ((∃𝑥(𝑥 = 𝑡 ∧ 𝜑) → ∀𝑥(𝑥 = 𝑡 → 𝜑)) → (∃𝑥(𝑥 = 𝑡 ∧ 𝜑) → ∀𝑥∀𝑥(𝑥 = 𝑡 → 𝜑))) |
3 | 19.38 1846 | . . . 4 ⊢ ((∃𝑥(𝑥 = 𝑡 ∧ 𝜑) → ∀𝑥∀𝑥(𝑥 = 𝑡 → 𝜑)) → ∀𝑥((𝑥 = 𝑡 ∧ 𝜑) → ∀𝑥(𝑥 = 𝑡 → 𝜑))) | |
4 | 2, 3 | syl 17 | . . 3 ⊢ ((∃𝑥(𝑥 = 𝑡 ∧ 𝜑) → ∀𝑥(𝑥 = 𝑡 → 𝜑)) → ∀𝑥((𝑥 = 𝑡 ∧ 𝜑) → ∀𝑥(𝑥 = 𝑡 → 𝜑))) |
5 | hbe1a 2146 | . . . . . 6 ⊢ (∃𝑥∀𝑥(𝑥 = 𝑡 → 𝜑) → ∀𝑥(𝑥 = 𝑡 → 𝜑)) | |
6 | 5, 1 | syl 17 | . . . . 5 ⊢ (∃𝑥∀𝑥(𝑥 = 𝑡 → 𝜑) → ∀𝑥∀𝑥(𝑥 = 𝑡 → 𝜑)) |
7 | bj-exlimg 34490 | . . . . 5 ⊢ ((∃𝑥∀𝑥(𝑥 = 𝑡 → 𝜑) → ∀𝑥∀𝑥(𝑥 = 𝑡 → 𝜑)) → (∀𝑥((𝑥 = 𝑡 ∧ 𝜑) → ∀𝑥(𝑥 = 𝑡 → 𝜑)) → (∃𝑥(𝑥 = 𝑡 ∧ 𝜑) → ∀𝑥∀𝑥(𝑥 = 𝑡 → 𝜑)))) | |
8 | 6, 7 | ax-mp 5 | . . . 4 ⊢ (∀𝑥((𝑥 = 𝑡 ∧ 𝜑) → ∀𝑥(𝑥 = 𝑡 → 𝜑)) → (∃𝑥(𝑥 = 𝑡 ∧ 𝜑) → ∀𝑥∀𝑥(𝑥 = 𝑡 → 𝜑))) |
9 | sp 2182 | . . . . 5 ⊢ (∀𝑥∀𝑥(𝑥 = 𝑡 → 𝜑) → ∀𝑥(𝑥 = 𝑡 → 𝜑)) | |
10 | 9 | imim2i 16 | . . . 4 ⊢ ((∃𝑥(𝑥 = 𝑡 ∧ 𝜑) → ∀𝑥∀𝑥(𝑥 = 𝑡 → 𝜑)) → (∃𝑥(𝑥 = 𝑡 ∧ 𝜑) → ∀𝑥(𝑥 = 𝑡 → 𝜑))) |
11 | 8, 10 | syl 17 | . . 3 ⊢ (∀𝑥((𝑥 = 𝑡 ∧ 𝜑) → ∀𝑥(𝑥 = 𝑡 → 𝜑)) → (∃𝑥(𝑥 = 𝑡 ∧ 𝜑) → ∀𝑥(𝑥 = 𝑡 → 𝜑))) |
12 | 4, 11 | impbii 212 | . 2 ⊢ ((∃𝑥(𝑥 = 𝑡 ∧ 𝜑) → ∀𝑥(𝑥 = 𝑡 → 𝜑)) ↔ ∀𝑥((𝑥 = 𝑡 ∧ 𝜑) → ∀𝑥(𝑥 = 𝑡 → 𝜑))) |
13 | impexp 454 | . . 3 ⊢ (((𝑥 = 𝑡 ∧ 𝜑) → ∀𝑥(𝑥 = 𝑡 → 𝜑)) ↔ (𝑥 = 𝑡 → (𝜑 → ∀𝑥(𝑥 = 𝑡 → 𝜑)))) | |
14 | 13 | albii 1827 | . 2 ⊢ (∀𝑥((𝑥 = 𝑡 ∧ 𝜑) → ∀𝑥(𝑥 = 𝑡 → 𝜑)) ↔ ∀𝑥(𝑥 = 𝑡 → (𝜑 → ∀𝑥(𝑥 = 𝑡 → 𝜑)))) |
15 | 12, 14 | bitri 278 | 1 ⊢ ((∃𝑥(𝑥 = 𝑡 ∧ 𝜑) → ∀𝑥(𝑥 = 𝑡 → 𝜑)) ↔ ∀𝑥(𝑥 = 𝑡 → (𝜑 → ∀𝑥(𝑥 = 𝑡 → 𝜑)))) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 209 ∧ wa 399 ∀wal 1541 ∃wex 1787 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1803 ax-4 1817 ax-5 1918 ax-6 1976 ax-7 2018 ax-10 2143 ax-12 2177 |
This theorem depends on definitions: df-bi 210 df-an 400 df-ex 1788 |
This theorem is referenced by: (None) |
Copyright terms: Public domain | W3C validator |