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 2021 from the standard axioms of predicate calculus, similar to PM's proof of alcom 2024 (PM*11.2). This proof requires that 𝑥 and 𝑦 be distinct. Axiom ax-11 2021 is used in the proof only through nfal 2139, nfsb 2428, sbal 2450, sb8 2412. See also ax11-pm 32007. (Contributed by BJ, 15-Sep-2018.) (Proof modification is discouraged.) |
Ref | Expression |
---|---|
ax11-pm2 | ⊢ (∀𝑥∀𝑦𝜑 → ∀𝑦∀𝑥𝜑) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | 2stdpc4 2342 | . . . . . 6 ⊢ (∀𝑥∀𝑦𝜑 → [𝑧 / 𝑥][𝑡 / 𝑦]𝜑) | |
2 | 1 | gen2 1714 | . . . . 5 ⊢ ∀𝑡∀𝑧(∀𝑥∀𝑦𝜑 → [𝑧 / 𝑥][𝑡 / 𝑦]𝜑) |
3 | nfv 1830 | . . . . . . . 8 ⊢ Ⅎ𝑡𝜑 | |
4 | 3 | nfal 2139 | . . . . . . 7 ⊢ Ⅎ𝑡∀𝑦𝜑 |
5 | 4 | nfal 2139 | . . . . . 6 ⊢ Ⅎ𝑡∀𝑥∀𝑦𝜑 |
6 | nfv 1830 | . . . . . . . 8 ⊢ Ⅎ𝑧𝜑 | |
7 | 6 | nfal 2139 | . . . . . . 7 ⊢ Ⅎ𝑧∀𝑦𝜑 |
8 | 7 | nfal 2139 | . . . . . 6 ⊢ Ⅎ𝑧∀𝑥∀𝑦𝜑 |
9 | 5, 8 | 2stdpc5 32004 | . . . . 5 ⊢ (∀𝑡∀𝑧(∀𝑥∀𝑦𝜑 → [𝑧 / 𝑥][𝑡 / 𝑦]𝜑) → (∀𝑥∀𝑦𝜑 → ∀𝑡∀𝑧[𝑧 / 𝑥][𝑡 / 𝑦]𝜑)) |
10 | 2, 9 | ax-mp 5 | . . . 4 ⊢ (∀𝑥∀𝑦𝜑 → ∀𝑡∀𝑧[𝑧 / 𝑥][𝑡 / 𝑦]𝜑) |
11 | 6 | nfsb 2428 | . . . . . 6 ⊢ Ⅎ𝑧[𝑡 / 𝑦]𝜑 |
12 | 11 | sb8 2412 | . . . . 5 ⊢ (∀𝑥[𝑡 / 𝑦]𝜑 ↔ ∀𝑧[𝑧 / 𝑥][𝑡 / 𝑦]𝜑) |
13 | 12 | albii 1737 | . . . 4 ⊢ (∀𝑡∀𝑥[𝑡 / 𝑦]𝜑 ↔ ∀𝑡∀𝑧[𝑧 / 𝑥][𝑡 / 𝑦]𝜑) |
14 | 10, 13 | sylibr 223 | . . 3 ⊢ (∀𝑥∀𝑦𝜑 → ∀𝑡∀𝑥[𝑡 / 𝑦]𝜑) |
15 | sbal 2450 | . . . 4 ⊢ ([𝑡 / 𝑦]∀𝑥𝜑 ↔ ∀𝑥[𝑡 / 𝑦]𝜑) | |
16 | 15 | albii 1737 | . . 3 ⊢ (∀𝑡[𝑡 / 𝑦]∀𝑥𝜑 ↔ ∀𝑡∀𝑥[𝑡 / 𝑦]𝜑) |
17 | 14, 16 | sylibr 223 | . 2 ⊢ (∀𝑥∀𝑦𝜑 → ∀𝑡[𝑡 / 𝑦]∀𝑥𝜑) |
18 | 3 | nfal 2139 | . . 3 ⊢ Ⅎ𝑡∀𝑥𝜑 |
19 | 18 | sb8 2412 | . 2 ⊢ (∀𝑦∀𝑥𝜑 ↔ ∀𝑡[𝑡 / 𝑦]∀𝑥𝜑) |
20 | 17, 19 | sylibr 223 | 1 ⊢ (∀𝑥∀𝑦𝜑 → ∀𝑦∀𝑥𝜑) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∀wal 1473 [wsb 1867 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1713 ax-4 1728 ax-5 1827 ax-6 1875 ax-7 1922 ax-10 2006 ax-11 2021 ax-12 2034 ax-13 2234 |
This theorem depends on definitions: df-bi 196 df-or 384 df-an 385 df-tru 1478 df-ex 1696 df-nf 1701 df-sb 1868 |
This theorem is referenced by: (None) |
Copyright terms: Public domain | W3C validator |