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	⊢ ( 𝑥 = 𝑦 → ( 𝑥 ∈ 𝑧 → 𝑦 ∈ 𝑧 ) )