Theorem ss-ax8 36794

Description: A proof of ax-8 2148 that does not rely on ax-8 2148. It employs df-ss 3923 to perform alpha-renaming and eliminates disjoint variable conditions using ax-9 2156. Contrary to in-ax8 36793, this proof does not rely on df-cleq 2757, 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 2049	. . . . . . 7 ⊢ (𝑥 = 𝑦 → (𝑥 = 𝑤 → 𝑦 = 𝑤))
2		ax12v2 2218	. . . . . . . . . . 11 ⊢ (𝑥 = 𝑤 → (𝑥 ∈ 𝑡 → ∀𝑥(𝑥 = 𝑤 → 𝑥 ∈ 𝑡)))
3	2	imp 412	. . . . . . . . . 10 ⊢ ((𝑥 = 𝑤 ∧ 𝑥 ∈ 𝑡) → ∀𝑥(𝑥 = 𝑤 → 𝑥 ∈ 𝑡))
4		equsb3 2141	. . . . . . . . . . . . . . 15 ⊢ ([𝑥 / 𝑣]𝑣 = 𝑤 ↔ 𝑥 = 𝑤)
5	4	bicomi 227	. . . . . . . . . . . . . 14 ⊢ (𝑥 = 𝑤 ↔ [𝑥 / 𝑣]𝑣 = 𝑤)
6	5	imbi1i 352	. . . . . . . . . . . . 13 ⊢ ((𝑥 = 𝑤 → 𝑥 ∈ 𝑡) ↔ ([𝑥 / 𝑣]𝑣 = 𝑤 → 𝑥 ∈ 𝑡))
7	6	albii 1852	. . . . . . . . . . . 12 ⊢ (∀𝑥(𝑥 = 𝑤 → 𝑥 ∈ 𝑡) ↔ ∀𝑥([𝑥 / 𝑣]𝑣 = 𝑤 → 𝑥 ∈ 𝑡))
8		df-clab 2744	. . . . . . . . . . . . . . . 16 ⊢ (𝑥 ∈ {𝑣 ∣ 𝑣 = 𝑤} ↔ [𝑥 / 𝑣]𝑣 = 𝑤)
9	8	bicomi 227	. . . . . . . . . . . . . . 15 ⊢ ([𝑥 / 𝑣]𝑣 = 𝑤 ↔ 𝑥 ∈ {𝑣 ∣ 𝑣 = 𝑤})
10	9	imbi1i 352	. . . . . . . . . . . . . 14 ⊢ (([𝑥 / 𝑣]𝑣 = 𝑤 → 𝑥 ∈ 𝑡) ↔ (𝑥 ∈ {𝑣 ∣ 𝑣 = 𝑤} → 𝑥 ∈ 𝑡))
11	10	albii 1852	. . . . . . . . . . . . 13 ⊢ (∀𝑥([𝑥 / 𝑣]𝑣 = 𝑤 → 𝑥 ∈ 𝑡) ↔ ∀𝑥(𝑥 ∈ {𝑣 ∣ 𝑣 = 𝑤} → 𝑥 ∈ 𝑡))
12		df-ss 3923	. . . . . . . . . . . . . 14 ⊢ ({𝑣 ∣ 𝑣 = 𝑤} ⊆ 𝑡 ↔ ∀𝑥(𝑥 ∈ {𝑣 ∣ 𝑣 = 𝑤} → 𝑥 ∈ 𝑡))
13		df-ss 3923	. . . . . . . . . . . . . 14 ⊢ ({𝑣 ∣ 𝑣 = 𝑤} ⊆ 𝑡 ↔ ∀𝑦(𝑦 ∈ {𝑣 ∣ 𝑣 = 𝑤} → 𝑦 ∈ 𝑡))
14	12, 13	bitr3i 280	. . . . . . . . . . . . 13 ⊢ (∀𝑥(𝑥 ∈ {𝑣 ∣ 𝑣 = 𝑤} → 𝑥 ∈ 𝑡) ↔ ∀𝑦(𝑦 ∈ {𝑣 ∣ 𝑣 = 𝑤} → 𝑦 ∈ 𝑡))
15		df-clab 2744	. . . . . . . . . . . . . . 15 ⊢ (𝑦 ∈ {𝑣 ∣ 𝑣 = 𝑤} ↔ [𝑦 / 𝑣]𝑣 = 𝑤)
16	15	imbi1i 352	. . . . . . . . . . . . . 14 ⊢ ((𝑦 ∈ {𝑣 ∣ 𝑣 = 𝑤} → 𝑦 ∈ 𝑡) ↔ ([𝑦 / 𝑣]𝑣 = 𝑤 → 𝑦 ∈ 𝑡))
17	16	albii 1852	. . . . . . . . . . . . 13 ⊢ (∀𝑦(𝑦 ∈ {𝑣 ∣ 𝑣 = 𝑤} → 𝑦 ∈ 𝑡) ↔ ∀𝑦([𝑦 / 𝑣]𝑣 = 𝑤 → 𝑦 ∈ 𝑡))
18	11, 14, 17	3bitri 300	. . . . . . . . . . . 12 ⊢ (∀𝑥([𝑥 / 𝑣]𝑣 = 𝑤 → 𝑥 ∈ 𝑡) ↔ ∀𝑦([𝑦 / 𝑣]𝑣 = 𝑤 → 𝑦 ∈ 𝑡))
19		equsb3 2141	. . . . . . . . . . . . . 14 ⊢ ([𝑦 / 𝑣]𝑣 = 𝑤 ↔ 𝑦 = 𝑤)
20	19	imbi1i 352	. . . . . . . . . . . . 13 ⊢ (([𝑦 / 𝑣]𝑣 = 𝑤 → 𝑦 ∈ 𝑡) ↔ (𝑦 = 𝑤 → 𝑦 ∈ 𝑡))
21	20	albii 1852	. . . . . . . . . . . 12 ⊢ (∀𝑦([𝑦 / 𝑣]𝑣 = 𝑤 → 𝑦 ∈ 𝑡) ↔ ∀𝑦(𝑦 = 𝑤 → 𝑦 ∈ 𝑡))
22	7, 18, 21	3bitri 300	. . . . . . . . . . 11 ⊢ (∀𝑥(𝑥 = 𝑤 → 𝑥 ∈ 𝑡) ↔ ∀𝑦(𝑦 = 𝑤 → 𝑦 ∈ 𝑡))
23	22	biimpi 219	. . . . . . . . . 10 ⊢ (∀𝑥(𝑥 = 𝑤 → 𝑥 ∈ 𝑡) → ∀𝑦(𝑦 = 𝑤 → 𝑦 ∈ 𝑡))
24		sp 2222	. . . . . . . . . 10 ⊢ (∀𝑦(𝑦 = 𝑤 → 𝑦 ∈ 𝑡) → (𝑦 = 𝑤 → 𝑦 ∈ 𝑡))
25	3, 23, 24	3syl 19	. . . . . . . . 9 ⊢ ((𝑥 = 𝑤 ∧ 𝑥 ∈ 𝑡) → (𝑦 = 𝑤 → 𝑦 ∈ 𝑡))
26	25	ex 418	. . . . . . . 8 ⊢ (𝑥 = 𝑤 → (𝑥 ∈ 𝑡 → (𝑦 = 𝑤 → 𝑦 ∈ 𝑡)))
27	26	com23 87	. . . . . . 7 ⊢ (𝑥 = 𝑤 → (𝑦 = 𝑤 → (𝑥 ∈ 𝑡 → 𝑦 ∈ 𝑡)))
28	1, 27	sylcom 31	. . . . . 6 ⊢ (𝑥 = 𝑦 → (𝑥 = 𝑤 → (𝑥 ∈ 𝑡 → 𝑦 ∈ 𝑡)))
29	28	com12 33	. . . . 5 ⊢ (𝑥 = 𝑤 → (𝑥 = 𝑦 → (𝑥 ∈ 𝑡 → 𝑦 ∈ 𝑡)))
30	29	equcoms 2053	. . . 4 ⊢ (𝑤 = 𝑥 → (𝑥 = 𝑦 → (𝑥 ∈ 𝑡 → 𝑦 ∈ 𝑡)))
31		ax6ev 2002	. . . 4 ⊢ ∃𝑤 𝑤 = 𝑥
32	30, 31	exlimiiv 1964	. . 3 ⊢ (𝑥 = 𝑦 → (𝑥 ∈ 𝑡 → 𝑦 ∈ 𝑡))
33		ax9 2160	. . . . 5 ⊢ (𝑧 = 𝑡 → (𝑥 ∈ 𝑧 → 𝑥 ∈ 𝑡))
34	33	equcoms 2053	. . . 4 ⊢ (𝑡 = 𝑧 → (𝑥 ∈ 𝑧 → 𝑥 ∈ 𝑡))
35		ax9 2160	. . . 4 ⊢ (𝑡 = 𝑧 → (𝑦 ∈ 𝑡 → 𝑦 ∈ 𝑧))
36	34, 35	imim12d 82	. . 3 ⊢ (𝑡 = 𝑧 → ((𝑥 ∈ 𝑡 → 𝑦 ∈ 𝑡) → (𝑥 ∈ 𝑧 → 𝑦 ∈ 𝑧)))
37	32, 36	syl5 35	. 2 ⊢ (𝑡 = 𝑧 → (𝑥 = 𝑦 → (𝑥 ∈ 𝑧 → 𝑦 ∈ 𝑧)))
38		ax6ev 2002	. 2 ⊢ ∃𝑡 𝑡 = 𝑧
39	37, 38	exlimiiv 1964	1 ⊢ (𝑥 = 𝑦 → (𝑥 ∈ 𝑧 → 𝑦 ∈ 𝑧))

This proof depends on syntax axioms:   → wi 4   ∧ wa 401  ∀wal 1568  [wsb 2099   ∈ wcel 2146  {cab 2743   ⊆ wss 3906

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-9 2156  ax-12 2216

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-sb 2100  df-clab 2744  df-ss 3923

This theorem is used by: (None)