Theorem ax9

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

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

Proof

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