Theorem ss-ax8 36183

Description: A proof of ax-8 2110 that does not rely on ax-8 2110. It employs df-ss 3993 to perform alpha-renaming and eliminates disjoint variable conditions using ax-9 2118. Contrary to in-ax8 36182, this proof does not rely on df-cleq 2732, 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 2015	. . . . . . 7 ⊢ (𝑥 = 𝑦 → (𝑥 = 𝑤 → 𝑦 = 𝑤))
2		ax12v2 2180	. . . . . . . . . . 11 ⊢ (𝑥 = 𝑤 → (𝑥 ∈ 𝑡 → ∀𝑥(𝑥 = 𝑤 → 𝑥 ∈ 𝑡)))
3	2	imp 406	. . . . . . . . . 10 ⊢ ((𝑥 = 𝑤 ∧ 𝑥 ∈ 𝑡) → ∀𝑥(𝑥 = 𝑤 → 𝑥 ∈ 𝑡))
4		equsb3 2103	. . . . . . . . . . . . . . 15 ⊢ ([𝑥 / 𝑣]𝑣 = 𝑤 ↔ 𝑥 = 𝑤)
5	4	bicomi 224	. . . . . . . . . . . . . 14 ⊢ (𝑥 = 𝑤 ↔ [𝑥 / 𝑣]𝑣 = 𝑤)
6	5	imbi1i 349	. . . . . . . . . . . . 13 ⊢ ((𝑥 = 𝑤 → 𝑥 ∈ 𝑡) ↔ ([𝑥 / 𝑣]𝑣 = 𝑤 → 𝑥 ∈ 𝑡))
7	6	albii 1817	. . . . . . . . . . . 12 ⊢ (∀𝑥(𝑥 = 𝑤 → 𝑥 ∈ 𝑡) ↔ ∀𝑥([𝑥 / 𝑣]𝑣 = 𝑤 → 𝑥 ∈ 𝑡))
8		df-clab 2718	. . . . . . . . . . . . . . . 16 ⊢ (𝑥 ∈ {𝑣 ∣ 𝑣 = 𝑤} ↔ [𝑥 / 𝑣]𝑣 = 𝑤)
9	8	bicomi 224	. . . . . . . . . . . . . . 15 ⊢ ([𝑥 / 𝑣]𝑣 = 𝑤 ↔ 𝑥 ∈ {𝑣 ∣ 𝑣 = 𝑤})
10	9	imbi1i 349	. . . . . . . . . . . . . 14 ⊢ (([𝑥 / 𝑣]𝑣 = 𝑤 → 𝑥 ∈ 𝑡) ↔ (𝑥 ∈ {𝑣 ∣ 𝑣 = 𝑤} → 𝑥 ∈ 𝑡))
11	10	albii 1817	. . . . . . . . . . . . 13 ⊢ (∀𝑥([𝑥 / 𝑣]𝑣 = 𝑤 → 𝑥 ∈ 𝑡) ↔ ∀𝑥(𝑥 ∈ {𝑣 ∣ 𝑣 = 𝑤} → 𝑥 ∈ 𝑡))
12		df-ss 3993	. . . . . . . . . . . . . 14 ⊢ ({𝑣 ∣ 𝑣 = 𝑤} ⊆ 𝑡 ↔ ∀𝑥(𝑥 ∈ {𝑣 ∣ 𝑣 = 𝑤} → 𝑥 ∈ 𝑡))
13		df-ss 3993	. . . . . . . . . . . . . 14 ⊢ ({𝑣 ∣ 𝑣 = 𝑤} ⊆ 𝑡 ↔ ∀𝑦(𝑦 ∈ {𝑣 ∣ 𝑣 = 𝑤} → 𝑦 ∈ 𝑡))
14	12, 13	bitr3i 277	. . . . . . . . . . . . 13 ⊢ (∀𝑥(𝑥 ∈ {𝑣 ∣ 𝑣 = 𝑤} → 𝑥 ∈ 𝑡) ↔ ∀𝑦(𝑦 ∈ {𝑣 ∣ 𝑣 = 𝑤} → 𝑦 ∈ 𝑡))
15		df-clab 2718	. . . . . . . . . . . . . . 15 ⊢ (𝑦 ∈ {𝑣 ∣ 𝑣 = 𝑤} ↔ [𝑦 / 𝑣]𝑣 = 𝑤)
16	15	imbi1i 349	. . . . . . . . . . . . . 14 ⊢ ((𝑦 ∈ {𝑣 ∣ 𝑣 = 𝑤} → 𝑦 ∈ 𝑡) ↔ ([𝑦 / 𝑣]𝑣 = 𝑤 → 𝑦 ∈ 𝑡))
17	16	albii 1817	. . . . . . . . . . . . 13 ⊢ (∀𝑦(𝑦 ∈ {𝑣 ∣ 𝑣 = 𝑤} → 𝑦 ∈ 𝑡) ↔ ∀𝑦([𝑦 / 𝑣]𝑣 = 𝑤 → 𝑦 ∈ 𝑡))
18	11, 14, 17	3bitri 297	. . . . . . . . . . . 12 ⊢ (∀𝑥([𝑥 / 𝑣]𝑣 = 𝑤 → 𝑥 ∈ 𝑡) ↔ ∀𝑦([𝑦 / 𝑣]𝑣 = 𝑤 → 𝑦 ∈ 𝑡))
19		equsb3 2103	. . . . . . . . . . . . . 14 ⊢ ([𝑦 / 𝑣]𝑣 = 𝑤 ↔ 𝑦 = 𝑤)
20	19	imbi1i 349	. . . . . . . . . . . . 13 ⊢ (([𝑦 / 𝑣]𝑣 = 𝑤 → 𝑦 ∈ 𝑡) ↔ (𝑦 = 𝑤 → 𝑦 ∈ 𝑡))
21	20	albii 1817	. . . . . . . . . . . 12 ⊢ (∀𝑦([𝑦 / 𝑣]𝑣 = 𝑤 → 𝑦 ∈ 𝑡) ↔ ∀𝑦(𝑦 = 𝑤 → 𝑦 ∈ 𝑡))
22	7, 18, 21	3bitri 297	. . . . . . . . . . 11 ⊢ (∀𝑥(𝑥 = 𝑤 → 𝑥 ∈ 𝑡) ↔ ∀𝑦(𝑦 = 𝑤 → 𝑦 ∈ 𝑡))
23	22	biimpi 216	. . . . . . . . . 10 ⊢ (∀𝑥(𝑥 = 𝑤 → 𝑥 ∈ 𝑡) → ∀𝑦(𝑦 = 𝑤 → 𝑦 ∈ 𝑡))
24		sp 2184	. . . . . . . . . 10 ⊢ (∀𝑦(𝑦 = 𝑤 → 𝑦 ∈ 𝑡) → (𝑦 = 𝑤 → 𝑦 ∈ 𝑡))
25	3, 23, 24	3syl 18	. . . . . . . . 9 ⊢ ((𝑥 = 𝑤 ∧ 𝑥 ∈ 𝑡) → (𝑦 = 𝑤 → 𝑦 ∈ 𝑡))
26	25	ex 412	. . . . . . . 8 ⊢ (𝑥 = 𝑤 → (𝑥 ∈ 𝑡 → (𝑦 = 𝑤 → 𝑦 ∈ 𝑡)))
27	26	com23 86	. . . . . . 7 ⊢ (𝑥 = 𝑤 → (𝑦 = 𝑤 → (𝑥 ∈ 𝑡 → 𝑦 ∈ 𝑡)))
28	1, 27	sylcom 30	. . . . . 6 ⊢ (𝑥 = 𝑦 → (𝑥 = 𝑤 → (𝑥 ∈ 𝑡 → 𝑦 ∈ 𝑡)))
29	28	com12 32	. . . . 5 ⊢ (𝑥 = 𝑤 → (𝑥 = 𝑦 → (𝑥 ∈ 𝑡 → 𝑦 ∈ 𝑡)))
30	29	equcoms 2019	. . . 4 ⊢ (𝑤 = 𝑥 → (𝑥 = 𝑦 → (𝑥 ∈ 𝑡 → 𝑦 ∈ 𝑡)))
31		ax6ev 1969	. . . 4 ⊢ ∃𝑤 𝑤 = 𝑥
32	30, 31	exlimiiv 1930	. . 3 ⊢ (𝑥 = 𝑦 → (𝑥 ∈ 𝑡 → 𝑦 ∈ 𝑡))
33		ax9 2122	. . . . 5 ⊢ (𝑧 = 𝑡 → (𝑥 ∈ 𝑧 → 𝑥 ∈ 𝑡))
34	33	equcoms 2019	. . . 4 ⊢ (𝑡 = 𝑧 → (𝑥 ∈ 𝑧 → 𝑥 ∈ 𝑡))
35		ax9 2122	. . . 4 ⊢ (𝑡 = 𝑧 → (𝑦 ∈ 𝑡 → 𝑦 ∈ 𝑧))
36	34, 35	imim12d 81	. . 3 ⊢ (𝑡 = 𝑧 → ((𝑥 ∈ 𝑡 → 𝑦 ∈ 𝑡) → (𝑥 ∈ 𝑧 → 𝑦 ∈ 𝑧)))
37	32, 36	syl5 34	. 2 ⊢ (𝑡 = 𝑧 → (𝑥 = 𝑦 → (𝑥 ∈ 𝑧 → 𝑦 ∈ 𝑧)))
38		ax6ev 1969	. 2 ⊢ ∃𝑡 𝑡 = 𝑧
39	37, 38	exlimiiv 1930	1 ⊢ (𝑥 = 𝑦 → (𝑥 ∈ 𝑧 → 𝑦 ∈ 𝑧))

Syntax hints:   → wi 4   ∧ wa 395  ∀wal 1535  [wsb 2064   ∈ wcel 2108  {cab 2717   ⊆ wss 3976

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-9 2118  ax-12 2178

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1778  df-sb 2065  df-clab 2718  df-ss 3993

This theorem is referenced by: (None)