Theorem ax9ALT

Description: Proof of ax-9 from Tarski's FOL and dfcleq . For a version not using ax-8 either, see eleq2w2 . 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	⊢ ( 𝑥 = 𝑦 → ( 𝑧 ∈ 𝑥 → 𝑧 ∈ 𝑦 ) )

Proof

Step	Hyp	Ref	Expression
1		dfcleq	⊢ ( 𝑥 = 𝑦 ↔ ∀ 𝑡 ( 𝑡 ∈ 𝑥 ↔ 𝑡 ∈ 𝑦 ) )
2	1	biimpi	⊢ ( 𝑥 = 𝑦 → ∀ 𝑡 ( 𝑡 ∈ 𝑥 ↔ 𝑡 ∈ 𝑦 ) )
3		biimp	⊢ ( ( 𝑡 ∈ 𝑥 ↔ 𝑡 ∈ 𝑦 ) → ( 𝑡 ∈ 𝑥 → 𝑡 ∈ 𝑦 ) )
4	2 3	sylg	⊢ ( 𝑥 = 𝑦 → ∀ 𝑡 ( 𝑡 ∈ 𝑥 → 𝑡 ∈ 𝑦 ) )
5		ax8	⊢ ( 𝑧 = 𝑡 → ( 𝑧 ∈ 𝑥 → 𝑡 ∈ 𝑥 ) )
6	5	equcoms	⊢ ( 𝑡 = 𝑧 → ( 𝑧 ∈ 𝑥 → 𝑡 ∈ 𝑥 ) )
7		ax8	⊢ ( 𝑡 = 𝑧 → ( 𝑡 ∈ 𝑦 → 𝑧 ∈ 𝑦 ) )
8	6 7	imim12d	⊢ ( 𝑡 = 𝑧 → ( ( 𝑡 ∈ 𝑥 → 𝑡 ∈ 𝑦 ) → ( 𝑧 ∈ 𝑥 → 𝑧 ∈ 𝑦 ) ) )
9	8	spimvw	⊢ ( ∀ 𝑡 ( 𝑡 ∈ 𝑥 → 𝑡 ∈ 𝑦 ) → ( 𝑧 ∈ 𝑥 → 𝑧 ∈ 𝑦 ) )
10	4 9	syl	⊢ ( 𝑥 = 𝑦 → ( 𝑧 ∈ 𝑥 → 𝑧 ∈ 𝑦 ) )