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