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	⊢ ( ( 𝑥 = 𝑦 ∧ 𝑧 = 𝑡 ) → ( 𝑥 ∈ 𝑧 → 𝑦 ∈ 𝑡 ) )

Proof

Step	Hyp	Ref	Expression
1		ax8	⊢ ( 𝑥 = 𝑦 → ( 𝑥 ∈ 𝑧 → 𝑦 ∈ 𝑧 ) )
2		ax9	⊢ ( 𝑧 = 𝑡 → ( 𝑦 ∈ 𝑧 → 𝑦 ∈ 𝑡 ) )
3	1 2	sylan9	⊢ ( ( 𝑥 = 𝑦 ∧ 𝑧 = 𝑡 ) → ( 𝑥 ∈ 𝑧 → 𝑦 ∈ 𝑡 ) )