![]() |
Mathbox for BJ |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > Mathboxes > bj-subst | Structured version Visualization version GIF version |
Description: Equivalent form of the
axiom of substitution bj-ax12 34369. Although both
sides need a DV condition on 𝑥, 𝑡 (or as in bj-ax12v3 34398 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 34435. Note that in the LHS, the reverse
implication holds by equs4 2428 (or equs4v 2007 if a DV condition is added on
𝑥,
𝑡 as in bj-ax12 34369).
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-subst | ⊢ ((∃𝑥(𝑥 = 𝑡 ∧ 𝜑) → ∀𝑥(𝑥 = 𝑡 → 𝜑)) ↔ ∀𝑥(𝑥 = 𝑡 → (𝜑 → ∀𝑥(𝑥 = 𝑡 → 𝜑)))) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | bj-modal4 34427 | . . . . 5 ⊢ (∀𝑥(𝑥 = 𝑡 → 𝜑) → ∀𝑥∀𝑥(𝑥 = 𝑡 → 𝜑)) | |
2 | 1 | imim2i 16 | . . . 4 ⊢ ((∃𝑥(𝑥 = 𝑡 ∧ 𝜑) → ∀𝑥(𝑥 = 𝑡 → 𝜑)) → (∃𝑥(𝑥 = 𝑡 ∧ 𝜑) → ∀𝑥∀𝑥(𝑥 = 𝑡 → 𝜑))) |
3 | 19.38 1841 | . . . 4 ⊢ ((∃𝑥(𝑥 = 𝑡 ∧ 𝜑) → ∀𝑥∀𝑥(𝑥 = 𝑡 → 𝜑)) → ∀𝑥((𝑥 = 𝑡 ∧ 𝜑) → ∀𝑥(𝑥 = 𝑡 → 𝜑))) | |
4 | 2, 3 | syl 17 | . . 3 ⊢ ((∃𝑥(𝑥 = 𝑡 ∧ 𝜑) → ∀𝑥(𝑥 = 𝑡 → 𝜑)) → ∀𝑥((𝑥 = 𝑡 ∧ 𝜑) → ∀𝑥(𝑥 = 𝑡 → 𝜑))) |
5 | hbe1a 2146 | . . . . . 6 ⊢ (∃𝑥∀𝑥(𝑥 = 𝑡 → 𝜑) → ∀𝑥(𝑥 = 𝑡 → 𝜑)) | |
6 | 5, 1 | syl 17 | . . . . 5 ⊢ (∃𝑥∀𝑥(𝑥 = 𝑡 → 𝜑) → ∀𝑥∀𝑥(𝑥 = 𝑡 → 𝜑)) |
7 | bj-exlimg 34335 | . . . . 5 ⊢ ((∃𝑥∀𝑥(𝑥 = 𝑡 → 𝜑) → ∀𝑥∀𝑥(𝑥 = 𝑡 → 𝜑)) → (∀𝑥((𝑥 = 𝑡 ∧ 𝜑) → ∀𝑥(𝑥 = 𝑡 → 𝜑)) → (∃𝑥(𝑥 = 𝑡 ∧ 𝜑) → ∀𝑥∀𝑥(𝑥 = 𝑡 → 𝜑)))) | |
8 | 6, 7 | ax-mp 5 | . . . 4 ⊢ (∀𝑥((𝑥 = 𝑡 ∧ 𝜑) → ∀𝑥(𝑥 = 𝑡 → 𝜑)) → (∃𝑥(𝑥 = 𝑡 ∧ 𝜑) → ∀𝑥∀𝑥(𝑥 = 𝑡 → 𝜑))) |
9 | sp 2181 | . . . . 5 ⊢ (∀𝑥∀𝑥(𝑥 = 𝑡 → 𝜑) → ∀𝑥(𝑥 = 𝑡 → 𝜑)) | |
10 | 9 | imim2i 16 | . . . 4 ⊢ ((∃𝑥(𝑥 = 𝑡 ∧ 𝜑) → ∀𝑥∀𝑥(𝑥 = 𝑡 → 𝜑)) → (∃𝑥(𝑥 = 𝑡 ∧ 𝜑) → ∀𝑥(𝑥 = 𝑡 → 𝜑))) |
11 | 8, 10 | syl 17 | . . 3 ⊢ (∀𝑥((𝑥 = 𝑡 ∧ 𝜑) → ∀𝑥(𝑥 = 𝑡 → 𝜑)) → (∃𝑥(𝑥 = 𝑡 ∧ 𝜑) → ∀𝑥(𝑥 = 𝑡 → 𝜑))) |
12 | 4, 11 | impbii 212 | . 2 ⊢ ((∃𝑥(𝑥 = 𝑡 ∧ 𝜑) → ∀𝑥(𝑥 = 𝑡 → 𝜑)) ↔ ∀𝑥((𝑥 = 𝑡 ∧ 𝜑) → ∀𝑥(𝑥 = 𝑡 → 𝜑))) |
13 | impexp 455 | . . 3 ⊢ (((𝑥 = 𝑡 ∧ 𝜑) → ∀𝑥(𝑥 = 𝑡 → 𝜑)) ↔ (𝑥 = 𝑡 → (𝜑 → ∀𝑥(𝑥 = 𝑡 → 𝜑)))) | |
14 | 13 | albii 1822 | . 2 ⊢ (∀𝑥((𝑥 = 𝑡 ∧ 𝜑) → ∀𝑥(𝑥 = 𝑡 → 𝜑)) ↔ ∀𝑥(𝑥 = 𝑡 → (𝜑 → ∀𝑥(𝑥 = 𝑡 → 𝜑)))) |
15 | 12, 14 | bitri 278 | 1 ⊢ ((∃𝑥(𝑥 = 𝑡 ∧ 𝜑) → ∀𝑥(𝑥 = 𝑡 → 𝜑)) ↔ ∀𝑥(𝑥 = 𝑡 → (𝜑 → ∀𝑥(𝑥 = 𝑡 → 𝜑)))) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 209 ∧ wa 400 ∀wal 1537 ∃wex 1782 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1798 ax-4 1812 ax-5 1912 ax-6 1971 ax-7 2016 ax-10 2143 ax-12 2176 |
This theorem depends on definitions: df-bi 210 df-an 401 df-ex 1783 |
This theorem is referenced by: (None) |
Copyright terms: Public domain | W3C validator |