axsepg2

Description: A generalization of ax-sep in which x and z need not be distinct. This theorem scheme bundles ax-sep with the degenerate instance E. y A. z ( z e. y <-> ( z e. z /\ ph ) ) which is satisfied by the existence of the empty set. Usage of this theorem is discouraged because it depends on ax-13 . (Contributed by BTernaryTau, 21-May-2026) (New usage is discouraged.)

		Ref	Expression
	Assertion	axsepg2	$⊢ \exists y \forall x (x \in y \leftrightarrow (x \in z \land φ))$

Proof

Step	Hyp	Ref	Expression
1		nfv	$⊢ Ⅎ y \neg \forall z z = x$
2		nfnae	$⊢ Ⅎ x \neg \forall z z = x$
3		nfcvf	$⊢ \neg \forall z z = x \to \underline{Ⅎ} z x$
4		nfcvd	$⊢ \neg \forall z z = x \to \underline{Ⅎ} z y$
5	3 4	nfeld	$⊢ \neg \forall z z = x \to Ⅎ z x \in y$
6		nfcvd	$⊢ \neg \forall z z = x \to \underline{Ⅎ} z w$
7	3 6	nfeld	$⊢ \neg \forall z z = x \to Ⅎ z x \in w$
8		nfvd	$⊢ \neg \forall z z = x \to Ⅎ z φ$
9	7 8	nfand	$⊢ \neg \forall z z = x \to Ⅎ z (x \in w \land φ)$
10	5 9	nfbid	$⊢ \neg \forall z z = x \to Ⅎ z (x \in y \leftrightarrow (x \in w \land φ))$
11	2 10	nfald	$⊢ \neg \forall z z = x \to Ⅎ z \forall x (x \in y \leftrightarrow (x \in w \land φ))$
12	1 11	nfexd	$⊢ \neg \forall z z = x \to Ⅎ z \exists y \forall x (x \in y \leftrightarrow (x \in w \land φ))$
13		nfvd	$⊢ \neg \forall z z = x \to Ⅎ w \exists y \forall x (x \in y \leftrightarrow (x \in z \land φ))$
14		dveeq2	$⊢ \neg \forall x x = z \to (w = z \to \forall x w = z)$
15	14	naecoms	$⊢ \neg \forall z z = x \to (w = z \to \forall x w = z)$
16		elequ2	$⊢ w = z \to (x \in w \leftrightarrow x \in z)$
17	16	anbi1d	$⊢ w = z \to ((x \in w \land φ) \leftrightarrow (x \in z \land φ))$
18	17	bibi2d	$⊢ w = z \to ((x \in y \leftrightarrow (x \in w \land φ)) \leftrightarrow (x \in y \leftrightarrow (x \in z \land φ)))$
19	18	biimpd	$⊢ w = z \to ((x \in y \leftrightarrow (x \in w \land φ)) \to (x \in y \leftrightarrow (x \in z \land φ)))$
20	19	al2imi	$⊢ \forall x w = z \to (\forall x (x \in y \leftrightarrow (x \in w \land φ)) \to \forall x (x \in y \leftrightarrow (x \in z \land φ)))$
21	20	eximdv	$⊢ \forall x w = z \to (\exists y \forall x (x \in y \leftrightarrow (x \in w \land φ)) \to \exists y \forall x (x \in y \leftrightarrow (x \in z \land φ)))$
22	15 21	syl6	$⊢ \neg \forall z z = x \to (w = z \to (\exists y \forall x (x \in y \leftrightarrow (x \in w \land φ)) \to \exists y \forall x (x \in y \leftrightarrow (x \in z \land φ))))$
23		elequ1	$⊢ z = x \to (z \in y \leftrightarrow x \in y)$
24		elequ1	$⊢ z = x \to (z \in z \leftrightarrow x \in z)$
25	24	anbi1d	$⊢ z = x \to ((z \in z \land φ) \leftrightarrow (x \in z \land φ))$
26	23 25	bibi12d	$⊢ z = x \to ((z \in y \leftrightarrow (z \in z \land φ)) \leftrightarrow (x \in y \leftrightarrow (x \in z \land φ)))$
27	26	biimpd	$⊢ z = x \to ((z \in y \leftrightarrow (z \in z \land φ)) \to (x \in y \leftrightarrow (x \in z \land φ)))$
28	27	al2imi	$⊢ \forall z z = x \to (\forall z (z \in y \leftrightarrow (z \in z \land φ)) \to \forall z (x \in y \leftrightarrow (x \in z \land φ)))$
29		axc11	$⊢ \forall z z = x \to (\forall z (x \in y \leftrightarrow (x \in z \land φ)) \to \forall x (x \in y \leftrightarrow (x \in z \land φ)))$
30	28 29	syld	$⊢ \forall z z = x \to (\forall z (z \in y \leftrightarrow (z \in z \land φ)) \to \forall x (x \in y \leftrightarrow (x \in z \land φ)))$
31	30	eximdv	$⊢ \forall z z = x \to (\exists y \forall z (z \in y \leftrightarrow (z \in z \land φ)) \to \exists y \forall x (x \in y \leftrightarrow (x \in z \land φ)))$
32		ax-sep	$⊢ \exists y \forall x (x \in y \leftrightarrow (x \in w \land φ))$
33	32	ax-gen	$⊢ \forall w \exists y \forall x (x \in y \leftrightarrow (x \in w \land φ))$
34		ax-nul	$⊢ \exists y \forall z \neg z \in y$
35		elirrv	$⊢ \neg z \in z$
36	35	intnanr	$⊢ \neg (z \in z \land φ)$
37	36	nbn	$⊢ \neg z \in y \leftrightarrow (z \in y \leftrightarrow (z \in z \land φ))$
38	37	biimpi	$⊢ \neg z \in y \to (z \in y \leftrightarrow (z \in z \land φ))$
39	38	alimi	$⊢ \forall z \neg z \in y \to \forall z (z \in y \leftrightarrow (z \in z \land φ))$
40	34 39	eximii	$⊢ \exists y \forall z (z \in y \leftrightarrow (z \in z \land φ))$
41	40	ax-gen	$⊢ \forall z \exists y \forall z (z \in y \leftrightarrow (z \in z \land φ))$
42	12 13 22 31 33 41	dvelimalcasei	$⊢ \forall z \exists y \forall x (x \in y \leftrightarrow (x \in z \land φ))$
43	42	spi	$⊢ \exists y \forall x (x \in y \leftrightarrow (x \in z \land φ))$

Metamath Proof Explorer

Theorem axsepg2

Proof