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

Metamath Proof Explorer

Theorem ss-ax8

Description: A proof of ax-8 that does not rely on ax-8 . It employs df-ss to perform alpha-renaming and eliminates disjoint variable conditions using ax-9 . Contrary to in-ax8 , this proof does not rely on df-cleq , therefore using fewer axioms . This method should not be applied to eliminate axiom dependencies. (Contributed by GG, 30-Aug-2025) (Proof modification is discouraged.) (New usage is discouraged.)

Ref Expression
Assertion ss-ax8 ( 𝑥 = 𝑦 → ( 𝑥 ∈ 𝑧 → 𝑦 ∈ 𝑧 ) )

Proof

Step Hyp Ref Expression
1 ax7 ⊢ ( 𝑥 = 𝑦 → ( 𝑥 = 𝑤 → 𝑦 = 𝑤 ) )
2 ax12v2 ⊢ ( 𝑥 = 𝑤 → ( 𝑥 ∈ 𝑡 → ∀ 𝑥 ( 𝑥 = 𝑤 → 𝑥 ∈ 𝑡 ) ) )
3 2 imp ⊢ ( ( 𝑥 = 𝑤 ∧ 𝑥 ∈ 𝑡 ) → ∀ 𝑥 ( 𝑥 = 𝑤 → 𝑥 ∈ 𝑡 ) )
4 equsb3 ⊢ ( [ 𝑥 / 𝑣 ] 𝑣 = 𝑤 ↔ 𝑥 = 𝑤 )
5 4 bicomi ⊢ ( 𝑥 = 𝑤 ↔ [ 𝑥 / 𝑣 ] 𝑣 = 𝑤 )
6 5 imbi1i ⊢ ( ( 𝑥 = 𝑤 → 𝑥 ∈ 𝑡 ) ↔ ( [ 𝑥 / 𝑣 ] 𝑣 = 𝑤 → 𝑥 ∈ 𝑡 ) )
7 6 albii ⊢ ( ∀ 𝑥 ( 𝑥 = 𝑤 → 𝑥 ∈ 𝑡 ) ↔ ∀ 𝑥 ( [ 𝑥 / 𝑣 ] 𝑣 = 𝑤 → 𝑥 ∈ 𝑡 ) )
8 df-clab ⊢ ( 𝑥 ∈ { 𝑣 ∣ 𝑣 = 𝑤 } ↔ [ 𝑥 / 𝑣 ] 𝑣 = 𝑤 )
9 8 bicomi ⊢ ( [ 𝑥 / 𝑣 ] 𝑣 = 𝑤 ↔ 𝑥 ∈ { 𝑣 ∣ 𝑣 = 𝑤 } )
10 9 imbi1i ⊢ ( ( [ 𝑥 / 𝑣 ] 𝑣 = 𝑤 → 𝑥 ∈ 𝑡 ) ↔ ( 𝑥 ∈ { 𝑣 ∣ 𝑣 = 𝑤 } → 𝑥 ∈ 𝑡 ) )
11 10 albii ⊢ ( ∀ 𝑥 ( [ 𝑥 / 𝑣 ] 𝑣 = 𝑤 → 𝑥 ∈ 𝑡 ) ↔ ∀ 𝑥 ( 𝑥 ∈ { 𝑣 ∣ 𝑣 = 𝑤 } → 𝑥 ∈ 𝑡 ) )
12 df-ss ⊢ ( { 𝑣 ∣ 𝑣 = 𝑤 } ⊆ 𝑡 ↔ ∀ 𝑥 ( 𝑥 ∈ { 𝑣 ∣ 𝑣 = 𝑤 } → 𝑥 ∈ 𝑡 ) )
13 df-ss ⊢ ( { 𝑣 ∣ 𝑣 = 𝑤 } ⊆ 𝑡 ↔ ∀ 𝑦 ( 𝑦 ∈ { 𝑣 ∣ 𝑣 = 𝑤 } → 𝑦 ∈ 𝑡 ) )
14 12 13 bitr3i ⊢ ( ∀ 𝑥 ( 𝑥 ∈ { 𝑣 ∣ 𝑣 = 𝑤 } → 𝑥 ∈ 𝑡 ) ↔ ∀ 𝑦 ( 𝑦 ∈ { 𝑣 ∣ 𝑣 = 𝑤 } → 𝑦 ∈ 𝑡 ) )
15 df-clab ⊢ ( 𝑦 ∈ { 𝑣 ∣ 𝑣 = 𝑤 } ↔ [ 𝑦 / 𝑣 ] 𝑣 = 𝑤 )
16 15 imbi1i ⊢ ( ( 𝑦 ∈ { 𝑣 ∣ 𝑣 = 𝑤 } → 𝑦 ∈ 𝑡 ) ↔ ( [ 𝑦 / 𝑣 ] 𝑣 = 𝑤 → 𝑦 ∈ 𝑡 ) )
17 16 albii ⊢ ( ∀ 𝑦 ( 𝑦 ∈ { 𝑣 ∣ 𝑣 = 𝑤 } → 𝑦 ∈ 𝑡 ) ↔ ∀ 𝑦 ( [ 𝑦 / 𝑣 ] 𝑣 = 𝑤 → 𝑦 ∈ 𝑡 ) )
18 11 14 17 3bitri ⊢ ( ∀ 𝑥 ( [ 𝑥 / 𝑣 ] 𝑣 = 𝑤 → 𝑥 ∈ 𝑡 ) ↔ ∀ 𝑦 ( [ 𝑦 / 𝑣 ] 𝑣 = 𝑤 → 𝑦 ∈ 𝑡 ) )
19 equsb3 ⊢ ( [ 𝑦 / 𝑣 ] 𝑣 = 𝑤 ↔ 𝑦 = 𝑤 )
20 19 imbi1i ⊢ ( ( [ 𝑦 / 𝑣 ] 𝑣 = 𝑤 → 𝑦 ∈ 𝑡 ) ↔ ( 𝑦 = 𝑤 → 𝑦 ∈ 𝑡 ) )
21 20 albii ⊢ ( ∀ 𝑦 ( [ 𝑦 / 𝑣 ] 𝑣 = 𝑤 → 𝑦 ∈ 𝑡 ) ↔ ∀ 𝑦 ( 𝑦 = 𝑤 → 𝑦 ∈ 𝑡 ) )
22 7 18 21 3bitri ⊢ ( ∀ 𝑥 ( 𝑥 = 𝑤 → 𝑥 ∈ 𝑡 ) ↔ ∀ 𝑦 ( 𝑦 = 𝑤 → 𝑦 ∈ 𝑡 ) )
23 22 biimpi ⊢ ( ∀ 𝑥 ( 𝑥 = 𝑤 → 𝑥 ∈ 𝑡 ) → ∀ 𝑦 ( 𝑦 = 𝑤 → 𝑦 ∈ 𝑡 ) )
24 sp ⊢ ( ∀ 𝑦 ( 𝑦 = 𝑤 → 𝑦 ∈ 𝑡 ) → ( 𝑦 = 𝑤 → 𝑦 ∈ 𝑡 ) )
25 3 23 24 3syl ⊢ ( ( 𝑥 = 𝑤 ∧ 𝑥 ∈ 𝑡 ) → ( 𝑦 = 𝑤 → 𝑦 ∈ 𝑡 ) )
26 25 ex ⊢ ( 𝑥 = 𝑤 → ( 𝑥 ∈ 𝑡 → ( 𝑦 = 𝑤 → 𝑦 ∈ 𝑡 ) ) )
27 26 com23 ⊢ ( 𝑥 = 𝑤 → ( 𝑦 = 𝑤 → ( 𝑥 ∈ 𝑡 → 𝑦 ∈ 𝑡 ) ) )
28 1 27 sylcom ⊢ ( 𝑥 = 𝑦 → ( 𝑥 = 𝑤 → ( 𝑥 ∈ 𝑡 → 𝑦 ∈ 𝑡 ) ) )
29 28 com12 ⊢ ( 𝑥 = 𝑤 → ( 𝑥 = 𝑦 → ( 𝑥 ∈ 𝑡 → 𝑦 ∈ 𝑡 ) ) )
30 29 equcoms ⊢ ( 𝑤 = 𝑥 → ( 𝑥 = 𝑦 → ( 𝑥 ∈ 𝑡 → 𝑦 ∈ 𝑡 ) ) )
31 ax6ev ⊢ ∃ 𝑤 𝑤 = 𝑥
32 30 31 exlimiiv ⊢ ( 𝑥 = 𝑦 → ( 𝑥 ∈ 𝑡 → 𝑦 ∈ 𝑡 ) )
33 ax9 ⊢ ( 𝑧 = 𝑡 → ( 𝑥 ∈ 𝑧 → 𝑥 ∈ 𝑡 ) )
34 33 equcoms ⊢ ( 𝑡 = 𝑧 → ( 𝑥 ∈ 𝑧 → 𝑥 ∈ 𝑡 ) )
35 ax9 ⊢ ( 𝑡 = 𝑧 → ( 𝑦 ∈ 𝑡 → 𝑦 ∈ 𝑧 ) )
36 34 35 imim12d ⊢ ( 𝑡 = 𝑧 → ( ( 𝑥 ∈ 𝑡 → 𝑦 ∈ 𝑡 ) → ( 𝑥 ∈ 𝑧 → 𝑦 ∈ 𝑧 ) ) )
37 32 36 syl5 ⊢ ( 𝑡 = 𝑧 → ( 𝑥 = 𝑦 → ( 𝑥 ∈ 𝑧 → 𝑦 ∈ 𝑧 ) ) )
38 ax6ev ⊢ ∃ 𝑡 𝑡 = 𝑧
39 37 38 exlimiiv ⊢ ( 𝑥 = 𝑦 → ( 𝑥 ∈ 𝑧 → 𝑦 ∈ 𝑧 ) )