Metamath Proof Explorer

Theorem axbnd

Description: Axiom of Bundling (intuitionistic logic axiom ax-bnd). In classical logic, this and axi12 are fairly straightforward consequences of axc9 . But in intuitionistic logic, it is not easy to add the extra A. x to axi12 and so we treat the two as separate axioms. Usage of this theorem is discouraged because it depends on ax-13 . (Contributed by Jim Kingdon, 22-Mar-2018) (Proof shortened by Wolf Lammen, 24-Apr-2023) (New usage is discouraged.)

Ref Expression
Assertion axbnd ⊢∀zz=x∨∀zz=y∨∀x∀zx=y→∀zx=y

Proof

Step Hyp Ref Expression
1 nfae ⊢Ⅎx∀zz=x
2 nfae ⊢Ⅎx∀zz=y
3 1 2 nfor ⊢Ⅎx∀zz=x∨∀zz=y
4 3 19.32 ⊢∀x∀zz=x∨∀zz=y∨∀zx=y→∀zx=y↔∀zz=x∨∀zz=y∨∀x∀zx=y→∀zx=y
5 orass ⊢∀zz=x∨∀zz=y∨∀x∀zx=y→∀zx=y↔∀zz=x∨∀zz=y∨∀x∀zx=y→∀zx=y
6 4 5 bitri ⊢∀x∀zz=x∨∀zz=y∨∀zx=y→∀zx=y↔∀zz=x∨∀zz=y∨∀x∀zx=y→∀zx=y
7 axi12 ⊢∀zz=x∨∀zz=y∨∀zx=y→∀zx=y
8 orass ⊢∀zz=x∨∀zz=y∨∀zx=y→∀zx=y↔∀zz=x∨∀zz=y∨∀zx=y→∀zx=y
9 7 8 mpbir ⊢∀zz=x∨∀zz=y∨∀zx=y→∀zx=y
10 6 9 mpgbi ⊢∀zz=x∨∀zz=y∨∀x∀zx=y→∀zx=y