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	$⊢ x = y \to (x \in z \to y \in z)$

Proof

Step	Hyp	Ref	Expression
1		ax7	$⊢ x = y \to (x = w \to y = w)$
2		ax12v2	$⊢ x = w \to ((x \in t \land x \in t) \to \forall x (x = w \to (x \in t \land x \in t)))$
3	2	imp	$⊢ (x = w \land (x \in t \land x \in t)) \to \forall x (x = w \to (x \in t \land x \in t))$
4		sb6	$⊢ [w/ x] (x \in t \land x \in t) \leftrightarrow \forall x (x = w \to (x \in t \land x \in t))$
5		df-in	$⊢ t \cap t = \{x \| (x \in t \land x \in t)\}$
6		df-in	$⊢ t \cap t = \{y \| (y \in t \land y \in t)\}$
7	5 6	eqtr3i	$⊢ \{x \| (x \in t \land x \in t)\} = \{y \| (y \in t \land y \in t)\}$
8		dfcleq	$⊢ \{x \| (x \in t \land x \in t)\} = \{y \| (y \in t \land y \in t)\} \leftrightarrow \forall w (w \in \{x \| (x \in t \land x \in t)\} \leftrightarrow w \in \{y \| (y \in t \land y \in t)\})$
9	7 8	mpbi	$⊢ \forall w (w \in \{x \| (x \in t \land x \in t)\} \leftrightarrow w \in \{y \| (y \in t \land y \in t)\})$
10	9	spi	$⊢ w \in \{x \| (x \in t \land x \in t)\} \leftrightarrow w \in \{y \| (y \in t \land y \in t)\}$
11		df-clab	$⊢ w \in \{x \| (x \in t \land x \in t)\} \leftrightarrow [w/ x] (x \in t \land x \in t)$
12		df-clab	$⊢ w \in \{y \| (y \in t \land y \in t)\} \leftrightarrow [w/ y] (y \in t \land y \in t)$
13	10 11 12	3bitr3i	$⊢ [w/ x] (x \in t \land x \in t) \leftrightarrow [w/ y] (y \in t \land y \in t)$
14	4 13	bitr3i	$⊢ \forall x (x = w \to (x \in t \land x \in t)) \leftrightarrow [w/ y] (y \in t \land y \in t)$
15		sb6	$⊢ [w/ y] (y \in t \land y \in t) \leftrightarrow \forall y (y = w \to (y \in t \land y \in t))$
16	14 15	sylbb	$⊢ \forall x (x = w \to (x \in t \land x \in t)) \to \forall y (y = w \to (y \in t \land y \in t))$
17		sp	$⊢ \forall y (y = w \to (y \in t \land y \in t)) \to (y = w \to (y \in t \land y \in t))$
18	3 16 17	3syl	$⊢ (x = w \land (x \in t \land x \in t)) \to (y = w \to (y \in t \land y \in t))$
19	18	ex	$⊢ x = w \to ((x \in t \land x \in t) \to (y = w \to (y \in t \land y \in t)))$
20	19	com23	$⊢ x = w \to (y = w \to ((x \in t \land x \in t) \to (y \in t \land y \in t)))$
21	1 20	sylcom	$⊢ x = y \to (x = w \to ((x \in t \land x \in t) \to (y \in t \land y \in t)))$
22	21	com12	$⊢ x = w \to (x = y \to ((x \in t \land x \in t) \to (y \in t \land y \in t)))$
23	22	equcoms	$⊢ w = x \to (x = y \to ((x \in t \land x \in t) \to (y \in t \land y \in t)))$
24		ax6ev	$⊢ \exists w w = x$
25	23 24	exlimiiv	$⊢ x = y \to ((x \in t \land x \in t) \to (y \in t \land y \in t))$
26		pm4.24	$⊢ x \in t \leftrightarrow (x \in t \land x \in t)$
27		pm4.24	$⊢ y \in t \leftrightarrow (y \in t \land y \in t)$
28	25 26 27	3imtr4g	$⊢ x = y \to (x \in t \to y \in t)$
29		ax9	$⊢ z = t \to (x \in z \to x \in t)$
30	29	equcoms	$⊢ t = z \to (x \in z \to x \in t)$
31		ax9	$⊢ t = z \to (y \in t \to y \in z)$
32	30 31	imim12d	$⊢ t = z \to ((x \in t \to y \in t) \to (x \in z \to y \in z))$
33	28 32	syl5	$⊢ t = z \to (x = y \to (x \in z \to y \in z))$
34		ax6ev	$⊢ \exists t t = z$
35	33 34	exlimiiv	$⊢ x = y \to (x \in z \to y \in z)$

Metamath Proof Explorer

Theorem in-ax8

Proof