This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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