Metamath Proof Explorer


Theorem bj-ax89

Description: A theorem which could be used as sole axiom for the non-logical predicate instead of ax-8 and ax-9 . Indeed, it is implied over propositional calculus by the conjunction of ax-8 and ax-9 , as proved here. In the other direction, one can prove ax-8 (respectively ax-9 ) from bj-ax89 by using mpan2 (respectively mpan ) and equid . TODO: move to main part. (Contributed by BJ, 3-Oct-2019)

Ref Expression
Assertion bj-ax89
|- ( ( x = y /\ z = t ) -> ( x e. z -> y e. t ) )

Proof

Step Hyp Ref Expression
1 ax8
 |-  ( x = y -> ( x e. z -> y e. z ) )
2 ax9
 |-  ( z = t -> ( y e. z -> y e. t ) )
3 1 2 sylan9
 |-  ( ( x = y /\ z = t ) -> ( x e. z -> y e. t ) )