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 
|- ( A. z z = x \/ ( A. z z = y \/ A. x A. z ( x = y -> A. z x = y ) ) )

Proof

Step Hyp Ref Expression
1 nfae 
 |-  F/ x A. z z = x
2 nfae 
 |-  F/ x A. z z = y
3 1 2 nfor 
 |-  F/ x ( A. z z = x \/ A. z z = y )
4 3 19.32 
 |-  ( A. x ( ( A. z z = x \/ A. z z = y ) \/ A. z ( x = y -> A. z x = y ) ) <-> ( ( A. z z = x \/ A. z z = y ) \/ A. x A. z ( x = y -> A. z x = y ) ) )
5 orass 
 |-  ( ( ( A. z z = x \/ A. z z = y ) \/ A. x A. z ( x = y -> A. z x = y ) ) <-> ( A. z z = x \/ ( A. z z = y \/ A. x A. z ( x = y -> A. z x = y ) ) ) )
6 4 5 bitri 
 |-  ( A. x ( ( A. z z = x \/ A. z z = y ) \/ A. z ( x = y -> A. z x = y ) ) <-> ( A. z z = x \/ ( A. z z = y \/ A. x A. z ( x = y -> A. z x = y ) ) ) )
7 axi12 
 |-  ( A. z z = x \/ ( A. z z = y \/ A. z ( x = y -> A. z x = y ) ) )
8 orass 
 |-  ( ( ( A. z z = x \/ A. z z = y ) \/ A. z ( x = y -> A. z x = y ) ) <-> ( A. z z = x \/ ( A. z z = y \/ A. z ( x = y -> A. z x = y ) ) ) )
9 7 8 mpbir 
 |-  ( ( A. z z = x \/ A. z z = y ) \/ A. z ( x = y -> A. z x = y ) )
10 6 9 mpgbi 
 |-  ( A. z z = x \/ ( A. z z = y \/ A. x A. z ( x = y -> A. z x = y ) ) )