![]() |
Mathbox for BJ |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > Mathboxes > ax11-pm2 | Structured version Visualization version GIF version |
Description: Proof of ax-11 2158 from the standard axioms of predicate calculus, similar to PM's proof of alcom 2160 (PM*11.2). This proof requires that 𝑥 and 𝑦 be distinct. Axiom ax-11 2158 is used in the proof only through nfal 2331, nfsb 2542, sbal 2163, sb8 2536. See also ax11-pm 34270. (Contributed by BJ, 15-Sep-2018.) (Proof modification is discouraged.) |
Ref | Expression |
---|---|
ax11-pm2 | ⊢ (∀𝑥∀𝑦𝜑 → ∀𝑦∀𝑥𝜑) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | 2stdpc4 2075 | . . . . . 6 ⊢ (∀𝑥∀𝑦𝜑 → [𝑧 / 𝑥][𝑡 / 𝑦]𝜑) | |
2 | 1 | gen2 1798 | . . . . 5 ⊢ ∀𝑡∀𝑧(∀𝑥∀𝑦𝜑 → [𝑧 / 𝑥][𝑡 / 𝑦]𝜑) |
3 | nfv 1915 | . . . . . . . 8 ⊢ Ⅎ𝑡𝜑 | |
4 | 3 | nfal 2331 | . . . . . . 7 ⊢ Ⅎ𝑡∀𝑦𝜑 |
5 | 4 | nfal 2331 | . . . . . 6 ⊢ Ⅎ𝑡∀𝑥∀𝑦𝜑 |
6 | nfv 1915 | . . . . . . . 8 ⊢ Ⅎ𝑧𝜑 | |
7 | 6 | nfal 2331 | . . . . . . 7 ⊢ Ⅎ𝑧∀𝑦𝜑 |
8 | 7 | nfal 2331 | . . . . . 6 ⊢ Ⅎ𝑧∀𝑥∀𝑦𝜑 |
9 | 5, 8 | 2stdpc5 34267 | . . . . 5 ⊢ (∀𝑡∀𝑧(∀𝑥∀𝑦𝜑 → [𝑧 / 𝑥][𝑡 / 𝑦]𝜑) → (∀𝑥∀𝑦𝜑 → ∀𝑡∀𝑧[𝑧 / 𝑥][𝑡 / 𝑦]𝜑)) |
10 | 2, 9 | ax-mp 5 | . . . 4 ⊢ (∀𝑥∀𝑦𝜑 → ∀𝑡∀𝑧[𝑧 / 𝑥][𝑡 / 𝑦]𝜑) |
11 | 6 | nfsbv 2338 | . . . . . 6 ⊢ Ⅎ𝑧[𝑡 / 𝑦]𝜑 |
12 | 11 | sb8v 2362 | . . . . 5 ⊢ (∀𝑥[𝑡 / 𝑦]𝜑 ↔ ∀𝑧[𝑧 / 𝑥][𝑡 / 𝑦]𝜑) |
13 | 12 | albii 1821 | . . . 4 ⊢ (∀𝑡∀𝑥[𝑡 / 𝑦]𝜑 ↔ ∀𝑡∀𝑧[𝑧 / 𝑥][𝑡 / 𝑦]𝜑) |
14 | 10, 13 | sylibr 237 | . . 3 ⊢ (∀𝑥∀𝑦𝜑 → ∀𝑡∀𝑥[𝑡 / 𝑦]𝜑) |
15 | sbal 2163 | . . . 4 ⊢ ([𝑡 / 𝑦]∀𝑥𝜑 ↔ ∀𝑥[𝑡 / 𝑦]𝜑) | |
16 | 15 | albii 1821 | . . 3 ⊢ (∀𝑡[𝑡 / 𝑦]∀𝑥𝜑 ↔ ∀𝑡∀𝑥[𝑡 / 𝑦]𝜑) |
17 | 14, 16 | sylibr 237 | . 2 ⊢ (∀𝑥∀𝑦𝜑 → ∀𝑡[𝑡 / 𝑦]∀𝑥𝜑) |
18 | 3 | nfal 2331 | . . 3 ⊢ Ⅎ𝑡∀𝑥𝜑 |
19 | 18 | sb8v 2362 | . 2 ⊢ (∀𝑦∀𝑥𝜑 ↔ ∀𝑡[𝑡 / 𝑦]∀𝑥𝜑) |
20 | 17, 19 | sylibr 237 | 1 ⊢ (∀𝑥∀𝑦𝜑 → ∀𝑦∀𝑥𝜑) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∀wal 1536 [wsb 2069 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1797 ax-4 1811 ax-5 1911 ax-6 1970 ax-7 2015 ax-10 2142 ax-11 2158 ax-12 2175 |
This theorem depends on definitions: df-bi 210 df-an 400 df-or 845 df-ex 1782 df-nf 1786 df-sb 2070 |
This theorem is referenced by: (None) |
Copyright terms: Public domain | W3C validator |