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

Metamath Proof Explorer

Theorem in-ax8

Description: A proof of ax-8 that does not rely on ax-8 . It employs df-in to perform alpha-renaming and eliminates disjoint variable conditions using ax-9 . Since the nature of this result is unclear, usage of this theorem is discouraged, and this method should not be applied to eliminate axiom dependencies. (Contributed by GG, 1-Aug-2025) (Proof modification is discouraged.) (New usage is discouraged.)

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

Proof

Step Hyp Ref Expression
1 ax7 ⊢ ( 𝑥 = 𝑦 → ( 𝑥 = 𝑤 → 𝑦 = 𝑤 ) )
2 ax12v2 ⊢ ( 𝑥 = 𝑤 → ( ( 𝑥 ∈ 𝑡 ∧ 𝑥 ∈ 𝑡 ) → ∀ 𝑥 ( 𝑥 = 𝑤 → ( 𝑥 ∈ 𝑡 ∧ 𝑥 ∈ 𝑡 ) ) ) )
3 2 imp ⊢ ( ( 𝑥 = 𝑤 ∧ ( 𝑥 ∈ 𝑡 ∧ 𝑥 ∈ 𝑡 ) ) → ∀ 𝑥 ( 𝑥 = 𝑤 → ( 𝑥 ∈ 𝑡 ∧ 𝑥 ∈ 𝑡 ) ) )
4 sb6 ⊢ ( [ 𝑤 / 𝑥 ] ( 𝑥 ∈ 𝑡 ∧ 𝑥 ∈ 𝑡 ) ↔ ∀ 𝑥 ( 𝑥 = 𝑤 → ( 𝑥 ∈ 𝑡 ∧ 𝑥 ∈ 𝑡 ) ) )
5 df-in ⊢ ( 𝑡 ∩ 𝑡 ) = { 𝑥 ∣ ( 𝑥 ∈ 𝑡 ∧ 𝑥 ∈ 𝑡 ) }
6 df-in ⊢ ( 𝑡 ∩ 𝑡 ) = { 𝑦 ∣ ( 𝑦 ∈ 𝑡 ∧ 𝑦 ∈ 𝑡 ) }
7 5 6 eqtr3i ⊢ { 𝑥 ∣ ( 𝑥 ∈ 𝑡 ∧ 𝑥 ∈ 𝑡 ) } = { 𝑦 ∣ ( 𝑦 ∈ 𝑡 ∧ 𝑦 ∈ 𝑡 ) }
8 dfcleq ⊢ ( { 𝑥 ∣ ( 𝑥 ∈ 𝑡 ∧ 𝑥 ∈ 𝑡 ) } = { 𝑦 ∣ ( 𝑦 ∈ 𝑡 ∧ 𝑦 ∈ 𝑡 ) } ↔ ∀ 𝑤 ( 𝑤 ∈ { 𝑥 ∣ ( 𝑥 ∈ 𝑡 ∧ 𝑥 ∈ 𝑡 ) } ↔ 𝑤 ∈ { 𝑦 ∣ ( 𝑦 ∈ 𝑡 ∧ 𝑦 ∈ 𝑡 ) } ) )
9 7 8 mpbi ⊢ ∀ 𝑤 ( 𝑤 ∈ { 𝑥 ∣ ( 𝑥 ∈ 𝑡 ∧ 𝑥 ∈ 𝑡 ) } ↔ 𝑤 ∈ { 𝑦 ∣ ( 𝑦 ∈ 𝑡 ∧ 𝑦 ∈ 𝑡 ) } )
10 9 spi ⊢ ( 𝑤 ∈ { 𝑥 ∣ ( 𝑥 ∈ 𝑡 ∧ 𝑥 ∈ 𝑡 ) } ↔ 𝑤 ∈ { 𝑦 ∣ ( 𝑦 ∈ 𝑡 ∧ 𝑦 ∈ 𝑡 ) } )
11 df-clab ⊢ ( 𝑤 ∈ { 𝑥 ∣ ( 𝑥 ∈ 𝑡 ∧ 𝑥 ∈ 𝑡 ) } ↔ [ 𝑤 / 𝑥 ] ( 𝑥 ∈ 𝑡 ∧ 𝑥 ∈ 𝑡 ) )
12 df-clab ⊢ ( 𝑤 ∈ { 𝑦 ∣ ( 𝑦 ∈ 𝑡 ∧ 𝑦 ∈ 𝑡 ) } ↔ [ 𝑤 / 𝑦 ] ( 𝑦 ∈ 𝑡 ∧ 𝑦 ∈ 𝑡 ) )
13 10 11 12 3bitr3i ⊢ ( [ 𝑤 / 𝑥 ] ( 𝑥 ∈ 𝑡 ∧ 𝑥 ∈ 𝑡 ) ↔ [ 𝑤 / 𝑦 ] ( 𝑦 ∈ 𝑡 ∧ 𝑦 ∈ 𝑡 ) )
14 4 13 bitr3i ⊢ ( ∀ 𝑥 ( 𝑥 = 𝑤 → ( 𝑥 ∈ 𝑡 ∧ 𝑥 ∈ 𝑡 ) ) ↔ [ 𝑤 / 𝑦 ] ( 𝑦 ∈ 𝑡 ∧ 𝑦 ∈ 𝑡 ) )
15 sb6 ⊢ ( [ 𝑤 / 𝑦 ] ( 𝑦 ∈ 𝑡 ∧ 𝑦 ∈ 𝑡 ) ↔ ∀ 𝑦 ( 𝑦 = 𝑤 → ( 𝑦 ∈ 𝑡 ∧ 𝑦 ∈ 𝑡 ) ) )
16 14 15 sylbb ⊢ ( ∀ 𝑥 ( 𝑥 = 𝑤 → ( 𝑥 ∈ 𝑡 ∧ 𝑥 ∈ 𝑡 ) ) → ∀ 𝑦 ( 𝑦 = 𝑤 → ( 𝑦 ∈ 𝑡 ∧ 𝑦 ∈ 𝑡 ) ) )
17 sp ⊢ ( ∀ 𝑦 ( 𝑦 = 𝑤 → ( 𝑦 ∈ 𝑡 ∧ 𝑦 ∈ 𝑡 ) ) → ( 𝑦 = 𝑤 → ( 𝑦 ∈ 𝑡 ∧ 𝑦 ∈ 𝑡 ) ) )
18 3 16 17 3syl ⊢ ( ( 𝑥 = 𝑤 ∧ ( 𝑥 ∈ 𝑡 ∧ 𝑥 ∈ 𝑡 ) ) → ( 𝑦 = 𝑤 → ( 𝑦 ∈ 𝑡 ∧ 𝑦 ∈ 𝑡 ) ) )
19 18 ex ⊢ ( 𝑥 = 𝑤 → ( ( 𝑥 ∈ 𝑡 ∧ 𝑥 ∈ 𝑡 ) → ( 𝑦 = 𝑤 → ( 𝑦 ∈ 𝑡 ∧ 𝑦 ∈ 𝑡 ) ) ) )
20 19 com23 ⊢ ( 𝑥 = 𝑤 → ( 𝑦 = 𝑤 → ( ( 𝑥 ∈ 𝑡 ∧ 𝑥 ∈ 𝑡 ) → ( 𝑦 ∈ 𝑡 ∧ 𝑦 ∈ 𝑡 ) ) ) )
21 1 20 sylcom ⊢ ( 𝑥 = 𝑦 → ( 𝑥 = 𝑤 → ( ( 𝑥 ∈ 𝑡 ∧ 𝑥 ∈ 𝑡 ) → ( 𝑦 ∈ 𝑡 ∧ 𝑦 ∈ 𝑡 ) ) ) )
22 21 com12 ⊢ ( 𝑥 = 𝑤 → ( 𝑥 = 𝑦 → ( ( 𝑥 ∈ 𝑡 ∧ 𝑥 ∈ 𝑡 ) → ( 𝑦 ∈ 𝑡 ∧ 𝑦 ∈ 𝑡 ) ) ) )
23 22 equcoms ⊢ ( 𝑤 = 𝑥 → ( 𝑥 = 𝑦 → ( ( 𝑥 ∈ 𝑡 ∧ 𝑥 ∈ 𝑡 ) → ( 𝑦 ∈ 𝑡 ∧ 𝑦 ∈ 𝑡 ) ) ) )
24 ax6ev ⊢ ∃ 𝑤 𝑤 = 𝑥
25 23 24 exlimiiv ⊢ ( 𝑥 = 𝑦 → ( ( 𝑥 ∈ 𝑡 ∧ 𝑥 ∈ 𝑡 ) → ( 𝑦 ∈ 𝑡 ∧ 𝑦 ∈ 𝑡 ) ) )
26 pm4.24 ⊢ ( 𝑥 ∈ 𝑡 ↔ ( 𝑥 ∈ 𝑡 ∧ 𝑥 ∈ 𝑡 ) )
27 pm4.24 ⊢ ( 𝑦 ∈ 𝑡 ↔ ( 𝑦 ∈ 𝑡 ∧ 𝑦 ∈ 𝑡 ) )
28 25 26 27 3imtr4g ⊢ ( 𝑥 = 𝑦 → ( 𝑥 ∈ 𝑡 → 𝑦 ∈ 𝑡 ) )
29 ax9 ⊢ ( 𝑧 = 𝑡 → ( 𝑥 ∈ 𝑧 → 𝑥 ∈ 𝑡 ) )
30 29 equcoms ⊢ ( 𝑡 = 𝑧 → ( 𝑥 ∈ 𝑧 → 𝑥 ∈ 𝑡 ) )
31 ax9 ⊢ ( 𝑡 = 𝑧 → ( 𝑦 ∈ 𝑡 → 𝑦 ∈ 𝑧 ) )
32 30 31 imim12d ⊢ ( 𝑡 = 𝑧 → ( ( 𝑥 ∈ 𝑡 → 𝑦 ∈ 𝑡 ) → ( 𝑥 ∈ 𝑧 → 𝑦 ∈ 𝑧 ) ) )
33 28 32 syl5 ⊢ ( 𝑡 = 𝑧 → ( 𝑥 = 𝑦 → ( 𝑥 ∈ 𝑧 → 𝑦 ∈ 𝑧 ) ) )
34 ax6ev ⊢ ∃ 𝑡 𝑡 = 𝑧
35 33 34 exlimiiv ⊢ ( 𝑥 = 𝑦 → ( 𝑥 ∈ 𝑧 → 𝑦 ∈ 𝑧 ) )