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 2151 from the standard axioms of predicate calculus, similar to PM's proof of alcom 2153 (PM*11.2). This proof requires that 𝑥 and 𝑦 be distinct. Axiom ax-11 2151 is used in the proof only through nfal 2333, nfsb 2558, sbal 2156, sb8 2552. See also ax11-pm 34052. (Contributed by BJ, 15-Sep-2018.) (Proof modification is discouraged.) |
Ref | Expression |
---|---|
ax11-pm2 | ⊢ (∀𝑥∀𝑦𝜑 → ∀𝑦∀𝑥𝜑) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | 2stdpc4 2066 | . . . . . 6 ⊢ (∀𝑥∀𝑦𝜑 → [𝑧 / 𝑥][𝑡 / 𝑦]𝜑) | |
2 | 1 | gen2 1788 | . . . . 5 ⊢ ∀𝑡∀𝑧(∀𝑥∀𝑦𝜑 → [𝑧 / 𝑥][𝑡 / 𝑦]𝜑) |
3 | nfv 1906 | . . . . . . . 8 ⊢ Ⅎ𝑡𝜑 | |
4 | 3 | nfal 2333 | . . . . . . 7 ⊢ Ⅎ𝑡∀𝑦𝜑 |
5 | 4 | nfal 2333 | . . . . . 6 ⊢ Ⅎ𝑡∀𝑥∀𝑦𝜑 |
6 | nfv 1906 | . . . . . . . 8 ⊢ Ⅎ𝑧𝜑 | |
7 | 6 | nfal 2333 | . . . . . . 7 ⊢ Ⅎ𝑧∀𝑦𝜑 |
8 | 7 | nfal 2333 | . . . . . 6 ⊢ Ⅎ𝑧∀𝑥∀𝑦𝜑 |
9 | 5, 8 | 2stdpc5 34049 | . . . . 5 ⊢ (∀𝑡∀𝑧(∀𝑥∀𝑦𝜑 → [𝑧 / 𝑥][𝑡 / 𝑦]𝜑) → (∀𝑥∀𝑦𝜑 → ∀𝑡∀𝑧[𝑧 / 𝑥][𝑡 / 𝑦]𝜑)) |
10 | 2, 9 | ax-mp 5 | . . . 4 ⊢ (∀𝑥∀𝑦𝜑 → ∀𝑡∀𝑧[𝑧 / 𝑥][𝑡 / 𝑦]𝜑) |
11 | 6 | nfsb 2558 | . . . . . 6 ⊢ Ⅎ𝑧[𝑡 / 𝑦]𝜑 |
12 | 11 | sb8 2552 | . . . . 5 ⊢ (∀𝑥[𝑡 / 𝑦]𝜑 ↔ ∀𝑧[𝑧 / 𝑥][𝑡 / 𝑦]𝜑) |
13 | 12 | albii 1811 | . . . 4 ⊢ (∀𝑡∀𝑥[𝑡 / 𝑦]𝜑 ↔ ∀𝑡∀𝑧[𝑧 / 𝑥][𝑡 / 𝑦]𝜑) |
14 | 10, 13 | sylibr 235 | . . 3 ⊢ (∀𝑥∀𝑦𝜑 → ∀𝑡∀𝑥[𝑡 / 𝑦]𝜑) |
15 | sbal 2156 | . . . 4 ⊢ ([𝑡 / 𝑦]∀𝑥𝜑 ↔ ∀𝑥[𝑡 / 𝑦]𝜑) | |
16 | 15 | albii 1811 | . . 3 ⊢ (∀𝑡[𝑡 / 𝑦]∀𝑥𝜑 ↔ ∀𝑡∀𝑥[𝑡 / 𝑦]𝜑) |
17 | 14, 16 | sylibr 235 | . 2 ⊢ (∀𝑥∀𝑦𝜑 → ∀𝑡[𝑡 / 𝑦]∀𝑥𝜑) |
18 | 3 | nfal 2333 | . . 3 ⊢ Ⅎ𝑡∀𝑥𝜑 |
19 | 18 | sb8 2552 | . 2 ⊢ (∀𝑦∀𝑥𝜑 ↔ ∀𝑡[𝑡 / 𝑦]∀𝑥𝜑) |
20 | 17, 19 | sylibr 235 | 1 ⊢ (∀𝑥∀𝑦𝜑 → ∀𝑦∀𝑥𝜑) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∀wal 1526 [wsb 2060 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1787 ax-4 1801 ax-5 1902 ax-6 1961 ax-7 2006 ax-10 2136 ax-11 2151 ax-12 2167 ax-13 2381 |
This theorem depends on definitions: df-bi 208 df-an 397 df-or 842 df-tru 1531 df-ex 1772 df-nf 1776 df-sb 2061 |
This theorem is referenced by: (None) |
Copyright terms: Public domain | W3C validator |