![]() |
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 2190 from the standard axioms of predicate calculus, similar to PM's proof of alcom 2193 (PM*11.2). This proof requires that 𝑥 and 𝑦 be distinct. Axiom ax-11 2190 is used in the proof only through nfal 2317, nfsb 2590, sbal 2610, sb8 2571. See also ax11-pm 33155. (Contributed by BJ, 15-Sep-2018.) (Proof modification is discouraged.) |
Ref | Expression |
---|---|
ax11-pm2 | ⊢ (∀𝑥∀𝑦𝜑 → ∀𝑦∀𝑥𝜑) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | 2stdpc4 2500 | . . . . . 6 ⊢ (∀𝑥∀𝑦𝜑 → [𝑧 / 𝑥][𝑡 / 𝑦]𝜑) | |
2 | 1 | gen2 1871 | . . . . 5 ⊢ ∀𝑡∀𝑧(∀𝑥∀𝑦𝜑 → [𝑧 / 𝑥][𝑡 / 𝑦]𝜑) |
3 | nfv 1995 | . . . . . . . 8 ⊢ Ⅎ𝑡𝜑 | |
4 | 3 | nfal 2317 | . . . . . . 7 ⊢ Ⅎ𝑡∀𝑦𝜑 |
5 | 4 | nfal 2317 | . . . . . 6 ⊢ Ⅎ𝑡∀𝑥∀𝑦𝜑 |
6 | nfv 1995 | . . . . . . . 8 ⊢ Ⅎ𝑧𝜑 | |
7 | 6 | nfal 2317 | . . . . . . 7 ⊢ Ⅎ𝑧∀𝑦𝜑 |
8 | 7 | nfal 2317 | . . . . . 6 ⊢ Ⅎ𝑧∀𝑥∀𝑦𝜑 |
9 | 5, 8 | 2stdpc5 33152 | . . . . 5 ⊢ (∀𝑡∀𝑧(∀𝑥∀𝑦𝜑 → [𝑧 / 𝑥][𝑡 / 𝑦]𝜑) → (∀𝑥∀𝑦𝜑 → ∀𝑡∀𝑧[𝑧 / 𝑥][𝑡 / 𝑦]𝜑)) |
10 | 2, 9 | ax-mp 5 | . . . 4 ⊢ (∀𝑥∀𝑦𝜑 → ∀𝑡∀𝑧[𝑧 / 𝑥][𝑡 / 𝑦]𝜑) |
11 | 6 | nfsb 2590 | . . . . . 6 ⊢ Ⅎ𝑧[𝑡 / 𝑦]𝜑 |
12 | 11 | sb8 2571 | . . . . 5 ⊢ (∀𝑥[𝑡 / 𝑦]𝜑 ↔ ∀𝑧[𝑧 / 𝑥][𝑡 / 𝑦]𝜑) |
13 | 12 | albii 1895 | . . . 4 ⊢ (∀𝑡∀𝑥[𝑡 / 𝑦]𝜑 ↔ ∀𝑡∀𝑧[𝑧 / 𝑥][𝑡 / 𝑦]𝜑) |
14 | 10, 13 | sylibr 224 | . . 3 ⊢ (∀𝑥∀𝑦𝜑 → ∀𝑡∀𝑥[𝑡 / 𝑦]𝜑) |
15 | sbal 2610 | . . . 4 ⊢ ([𝑡 / 𝑦]∀𝑥𝜑 ↔ ∀𝑥[𝑡 / 𝑦]𝜑) | |
16 | 15 | albii 1895 | . . 3 ⊢ (∀𝑡[𝑡 / 𝑦]∀𝑥𝜑 ↔ ∀𝑡∀𝑥[𝑡 / 𝑦]𝜑) |
17 | 14, 16 | sylibr 224 | . 2 ⊢ (∀𝑥∀𝑦𝜑 → ∀𝑡[𝑡 / 𝑦]∀𝑥𝜑) |
18 | 3 | nfal 2317 | . . 3 ⊢ Ⅎ𝑡∀𝑥𝜑 |
19 | 18 | sb8 2571 | . 2 ⊢ (∀𝑦∀𝑥𝜑 ↔ ∀𝑡[𝑡 / 𝑦]∀𝑥𝜑) |
20 | 17, 19 | sylibr 224 | 1 ⊢ (∀𝑥∀𝑦𝜑 → ∀𝑦∀𝑥𝜑) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∀wal 1629 [wsb 2049 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1870 ax-4 1885 ax-5 1991 ax-6 2057 ax-7 2093 ax-10 2174 ax-11 2190 ax-12 2203 ax-13 2408 |
This theorem depends on definitions: df-bi 197 df-an 383 df-or 829 df-tru 1634 df-ex 1853 df-nf 1858 df-sb 2050 |
This theorem is referenced by: (None) |
Copyright terms: Public domain | W3C validator |