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	$$⊢\left(x=y\wedge z=t\right)\to \left(x\in z\to y\in t\right)$$

Proof

Step	Hyp	Ref	Expression
1		ax8	$$⊢x=y\to \left(x\in z\to y\in z\right)$$
2		ax9	$$⊢z=t\to \left(y\in z\to y\in t\right)$$
3	1 2	sylan9	$$⊢\left(x=y\wedge z=t\right)\to \left(x\in z\to y\in t\right)$$