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	$⊢ 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 \to \forall x (x = w \to x \in t))$
3	2	imp	$⊢ (x = w \land x \in t) \to \forall x (x = w \to x \in t)$
4		equsb3	$⊢ [x/ v] v = w \leftrightarrow x = w$
5	4	bicomi	$⊢ x = w \leftrightarrow [x/ v] v = w$
6	5	imbi1i	$⊢ (x = w \to x \in t) \leftrightarrow ([x/ v] v = w \to x \in t)$
7	6	albii	$⊢ \forall x (x = w \to x \in t) \leftrightarrow \forall x ([x/ v] v = w \to x \in t)$
8		df-clab	$⊢ x \in \{v \| v = w\} \leftrightarrow [x/ v] v = w$
9	8	bicomi	$⊢ [x/ v] v = w \leftrightarrow x \in \{v \| v = w\}$
10	9	imbi1i	$⊢ ([x/ v] v = w \to x \in t) \leftrightarrow (x \in \{v \| v = w\} \to x \in t)$
11	10	albii	$⊢ \forall x ([x/ v] v = w \to x \in t) \leftrightarrow \forall x (x \in \{v \| v = w\} \to x \in t)$
12		df-ss	$⊢ \{v \| v = w\} \subseteq t \leftrightarrow \forall x (x \in \{v \| v = w\} \to x \in t)$
13		df-ss	$⊢ \{v \| v = w\} \subseteq t \leftrightarrow \forall y (y \in \{v \| v = w\} \to y \in t)$
14	12 13	bitr3i	$⊢ \forall x (x \in \{v \| v = w\} \to x \in t) \leftrightarrow \forall y (y \in \{v \| v = w\} \to y \in t)$
15		df-clab	$⊢ y \in \{v \| v = w\} \leftrightarrow [y/ v] v = w$
16	15	imbi1i	$⊢ (y \in \{v \| v = w\} \to y \in t) \leftrightarrow ([y/ v] v = w \to y \in t)$
17	16	albii	$⊢ \forall y (y \in \{v \| v = w\} \to y \in t) \leftrightarrow \forall y ([y/ v] v = w \to y \in t)$
18	11 14 17	3bitri	$⊢ \forall x ([x/ v] v = w \to x \in t) \leftrightarrow \forall y ([y/ v] v = w \to y \in t)$
19		equsb3	$⊢ [y/ v] v = w \leftrightarrow y = w$
20	19	imbi1i	$⊢ ([y/ v] v = w \to y \in t) \leftrightarrow (y = w \to y \in t)$
21	20	albii	$⊢ \forall y ([y/ v] v = w \to y \in t) \leftrightarrow \forall y (y = w \to y \in t)$
22	7 18 21	3bitri	$⊢ \forall x (x = w \to x \in t) \leftrightarrow \forall y (y = w \to y \in t)$
23	22	biimpi	$⊢ \forall x (x = w \to x \in t) \to \forall y (y = w \to y \in t)$
24		sp	$⊢ \forall y (y = w \to y \in t) \to (y = w \to y \in t)$
25	3 23 24	3syl	$⊢ (x = w \land x \in t) \to (y = w \to y \in t)$
26	25	ex	$⊢ x = w \to (x \in t \to (y = w \to y \in t))$
27	26	com23	$⊢ x = w \to (y = w \to (x \in t \to y \in t))$
28	1 27	sylcom	$⊢ x = y \to (x = w \to (x \in t \to y \in t))$
29	28	com12	$⊢ x = w \to (x = y \to (x \in t \to y \in t))$
30	29	equcoms	$⊢ w = x \to (x = y \to (x \in t \to y \in t))$
31		ax6ev	$⊢ \exists w w = x$
32	30 31	exlimiiv	$⊢ x = y \to (x \in t \to y \in t)$
33		ax9	$⊢ z = t \to (x \in z \to x \in t)$
34	33	equcoms	$⊢ t = z \to (x \in z \to x \in t)$
35		ax9	$⊢ t = z \to (y \in t \to y \in z)$
36	34 35	imim12d	$⊢ t = z \to ((x \in t \to y \in t) \to (x \in z \to y \in z))$
37	32 36	syl5	$⊢ t = z \to (x = y \to (x \in z \to y \in z))$
38		ax6ev	$⊢ \exists t t = z$
39	37 38	exlimiiv	$⊢ x = y \to (x \in z \to y \in z)$

Metamath Proof Explorer

Theorem ss-ax8

Proof