Theorem ax8

Description: Proof of ax-8 from ax8v1 and ax8v2 , proving sufficiency of the conjunction of the latter two weakened versions of ax8v , which is itself a weakened version of ax-8 . (Contributed by BJ, 7-Dec-2020) (Proof shortened by Wolf Lammen, 11-Apr-2021)

	Ref	Expression
Assertion	ax8	$$⊢x=y\to \left(x\in z\to y\in z\right)$$

Proof

Step	Hyp	Ref	Expression
1		equvinv	$$⊢x=y\leftrightarrow \exists t\left(t=x\wedge t=y\right)$$
2		ax8v2	$$⊢x=t\to \left(x\in z\to t\in z\right)$$
3	2	equcoms	$$⊢t=x\to \left(x\in z\to t\in z\right)$$
4		ax8v1	$$⊢t=y\to \left(t\in z\to y\in z\right)$$
5	3 4	sylan9	$$⊢\left(t=x\wedge t=y\right)\to \left(x\in z\to y\in z\right)$$
6	5	exlimiv	$$⊢\exists t\left(t=x\wedge t=y\right)\to \left(x\in z\to y\in z\right)$$
7	1 6	sylbi	$$⊢x=y\to \left(x\in z\to y\in z\right)$$