Theorem ss-ax8 36453

Description: A proof of ax-8 2121 that does not rely on ax-8 2121. It employs df-ss 3900 to perform alpha-renaming and eliminates disjoint variable conditions using ax-9 2129. Contrary to in-ax8 36452, this proof does not rely on df-cleq 2731, 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.)

Assertion

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

Proof of Theorem ss-ax8

Dummy variables 𝑡 𝑤 𝑣 are mutually distinct and distinct from all other variables.

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

Syntax hints:   → wi 4   ∧ wa 396  ∀wal 1545  [wsb 2073   ∈ wcel 2119  {cab 2717   ⊆ wss 3883

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-9 2129  ax-12 2189

This theorem depends on definitions:  df-bi 208  df-an 397  df-ex 1787  df-sb 2074  df-clab 2718  df-ss 3900

This theorem is referenced by: (None)