![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > axbnd | Structured version Visualization version GIF version |
Description: Axiom of Bundling (intuitionistic logic axiom ax-bnd). In classical logic, this and axi12 2765 are fairly straightforward consequences of axc9 2355. But in intuitionistic logic, it is not easy to add the extra ∀𝑥 to axi12 2765 and so we treat the two as separate axioms. (Contributed by Jim Kingdon, 22-Mar-2018.) (Proof shortened by Wolf Lammen, 24-Apr-2023.) |
Ref | Expression |
---|---|
axbnd | ⊢ (∀𝑧 𝑧 = 𝑥 ∨ (∀𝑧 𝑧 = 𝑦 ∨ ∀𝑥∀𝑧(𝑥 = 𝑦 → ∀𝑧 𝑥 = 𝑦))) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | nfae 2412 | . . . . 5 ⊢ Ⅎ𝑥∀𝑧 𝑧 = 𝑥 | |
2 | nfae 2412 | . . . . 5 ⊢ Ⅎ𝑥∀𝑧 𝑧 = 𝑦 | |
3 | 1, 2 | nfor 1886 | . . . 4 ⊢ Ⅎ𝑥(∀𝑧 𝑧 = 𝑥 ∨ ∀𝑧 𝑧 = 𝑦) |
4 | 3 | 19.32 2200 | . . 3 ⊢ (∀𝑥((∀𝑧 𝑧 = 𝑥 ∨ ∀𝑧 𝑧 = 𝑦) ∨ ∀𝑧(𝑥 = 𝑦 → ∀𝑧 𝑥 = 𝑦)) ↔ ((∀𝑧 𝑧 = 𝑥 ∨ ∀𝑧 𝑧 = 𝑦) ∨ ∀𝑥∀𝑧(𝑥 = 𝑦 → ∀𝑧 𝑥 = 𝑦))) |
5 | orass 916 | . . 3 ⊢ (((∀𝑧 𝑧 = 𝑥 ∨ ∀𝑧 𝑧 = 𝑦) ∨ ∀𝑥∀𝑧(𝑥 = 𝑦 → ∀𝑧 𝑥 = 𝑦)) ↔ (∀𝑧 𝑧 = 𝑥 ∨ (∀𝑧 𝑧 = 𝑦 ∨ ∀𝑥∀𝑧(𝑥 = 𝑦 → ∀𝑧 𝑥 = 𝑦)))) | |
6 | 4, 5 | bitri 276 | . 2 ⊢ (∀𝑥((∀𝑧 𝑧 = 𝑥 ∨ ∀𝑧 𝑧 = 𝑦) ∨ ∀𝑧(𝑥 = 𝑦 → ∀𝑧 𝑥 = 𝑦)) ↔ (∀𝑧 𝑧 = 𝑥 ∨ (∀𝑧 𝑧 = 𝑦 ∨ ∀𝑥∀𝑧(𝑥 = 𝑦 → ∀𝑧 𝑥 = 𝑦)))) |
7 | axi12 2765 | . . 3 ⊢ (∀𝑧 𝑧 = 𝑥 ∨ (∀𝑧 𝑧 = 𝑦 ∨ ∀𝑧(𝑥 = 𝑦 → ∀𝑧 𝑥 = 𝑦))) | |
8 | orass 916 | . . 3 ⊢ (((∀𝑧 𝑧 = 𝑥 ∨ ∀𝑧 𝑧 = 𝑦) ∨ ∀𝑧(𝑥 = 𝑦 → ∀𝑧 𝑥 = 𝑦)) ↔ (∀𝑧 𝑧 = 𝑥 ∨ (∀𝑧 𝑧 = 𝑦 ∨ ∀𝑧(𝑥 = 𝑦 → ∀𝑧 𝑥 = 𝑦)))) | |
9 | 7, 8 | mpbir 232 | . 2 ⊢ ((∀𝑧 𝑧 = 𝑥 ∨ ∀𝑧 𝑧 = 𝑦) ∨ ∀𝑧(𝑥 = 𝑦 → ∀𝑧 𝑥 = 𝑦)) |
10 | 6, 9 | mpgbi 1780 | 1 ⊢ (∀𝑧 𝑧 = 𝑥 ∨ (∀𝑧 𝑧 = 𝑦 ∨ ∀𝑥∀𝑧(𝑥 = 𝑦 → ∀𝑧 𝑥 = 𝑦))) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∨ wo 842 ∀wal 1520 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1777 ax-4 1791 ax-5 1888 ax-6 1947 ax-7 1992 ax-10 2112 ax-11 2126 ax-12 2141 ax-13 2344 |
This theorem depends on definitions: df-bi 208 df-an 397 df-or 843 df-tru 1525 df-ex 1762 df-nf 1766 |
This theorem is referenced by: (None) |
Copyright terms: Public domain | W3C validator |