![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > sbalex | Structured version Visualization version GIF version |
Description: Equivalence of two ways
to express proper substitution of a setvar for
another setvar disjoint from it in a formula. This proof of their
equivalence does not use df-sb 2062.
That both sides of the biconditional express proper substitution is proved by sb5 2273 and sb6 2082. The implication "to the left" is equs4v 1996 and does not require ax-10 2138 nor ax-12 2174. It also holds without disjoint variable condition if we allow more axioms (see equs4 2418). Theorem 6.2 of [Quine] p. 40. Theorem equs5 2462 replaces the disjoint variable condition with a distinctor antecedent. Theorem equs45f 2461 replaces the disjoint variable condition on 𝑥, 𝑡 with the nonfreeness hypothesis of 𝑡 in 𝜑. (Contributed by NM, 14-Apr-2008.) Revised to use equsexv 2265 in place of equsex 2420 in order to remove dependency on ax-13 2374. (Revised by BJ, 20-Dec-2020.) Revise to remove dependency on df-sb 2062. (Revised by BJ, 21-Sep-2024.) (Proof shortened by SN, 14-Aug-2025.) |
Ref | Expression |
---|---|
sbalex | ⊢ (∃𝑥(𝑥 = 𝑡 ∧ 𝜑) ↔ ∀𝑥(𝑥 = 𝑡 → 𝜑)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | nfe1 2147 | . . 3 ⊢ Ⅎ𝑥∃𝑥(𝑥 = 𝑡 ∧ 𝜑) | |
2 | ax12ev2 2177 | . . 3 ⊢ (∃𝑥(𝑥 = 𝑡 ∧ 𝜑) → (𝑥 = 𝑡 → 𝜑)) | |
3 | 1, 2 | alrimi 2210 | . 2 ⊢ (∃𝑥(𝑥 = 𝑡 ∧ 𝜑) → ∀𝑥(𝑥 = 𝑡 → 𝜑)) |
4 | equs4v 1996 | . 2 ⊢ (∀𝑥(𝑥 = 𝑡 → 𝜑) → ∃𝑥(𝑥 = 𝑡 ∧ 𝜑)) | |
5 | 3, 4 | impbii 209 | 1 ⊢ (∃𝑥(𝑥 = 𝑡 ∧ 𝜑) ↔ ∀𝑥(𝑥 = 𝑡 → 𝜑)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 206 ∧ wa 395 ∀wal 1534 ∃wex 1775 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1791 ax-4 1805 ax-5 1907 ax-6 1964 ax-7 2004 ax-10 2138 ax-12 2174 |
This theorem depends on definitions: df-bi 207 df-an 396 df-ex 1776 df-nf 1780 |
This theorem is referenced by: equsexvOLD 2266 sb5 2273 dfsb7 2277 alexeqg 3650 dfdif3OLD 4127 pm13.196a 44409 |
Copyright terms: Public domain | W3C validator |