Theorem ax9ALT

Description: Proof of ax-9 from Tarski's FOL and dfcleq . For a version not using ax-8 either, see bj-ax9 . This shows that dfcleq is too powerful to be used as a definition instead of df-cleq . Note that ax-ext is also a direct consequence of dfcleq (as an instance of its forward implication). (Contributed by BJ, 24-Jun-2019) (Proof modification is discouraged.) (New usage is discouraged.)

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

Proof

Step	Hyp	Ref	Expression
1		dfcleq	$$⊢x=y\leftrightarrow \forall t\left(t\in x\leftrightarrow t\in y\right)$$
2	1	biimpi	$$⊢x=y\to \forall t\left(t\in x\leftrightarrow t\in y\right)$$
3		biimp	$$⊢\left(t\in x\leftrightarrow t\in y\right)\to \left(t\in x\to t\in y\right)$$
4	2 3	sylg	$$⊢x=y\to \forall t\left(t\in x\to t\in y\right)$$
5		ax8	$$⊢z=t\to \left(z\in x\to t\in x\right)$$
6	5	equcoms	$$⊢t=z\to \left(z\in x\to t\in x\right)$$
7		ax8	$$⊢t=z\to \left(t\in y\to z\in y\right)$$
8	6 7	imim12d	$$⊢t=z\to \left(\left(t\in x\to t\in y\right)\to \left(z\in x\to z\in y\right)\right)$$
9	8	spimvw	$$⊢\forall t\left(t\in x\to t\in y\right)\to \left(z\in x\to z\in y\right)$$
10	4 9	syl	$$⊢x=y\to \left(z\in x\to z\in y\right)$$