axsepg3

Description: A generalization of ax-sep in which y and z need not be distinct. This theorem scheme bundles ax-sep with the degenerate instance E. y A. x ( x e. y <-> ( x e. y /\ 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, 3-Aug-2025) (New usage is discouraged.)

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

Proof

Step	Hyp	Ref	Expression
1		nfv	$⊢ Ⅎ x \neg \forall y y = z$
2		nfvd	$⊢ \neg \forall y y = z \to Ⅎ y x \in w$
3		nfcvf	$⊢ \neg \forall y y = z \to \underline{Ⅎ} y z$
4	3	nfcrd	$⊢ \neg \forall y y = z \to Ⅎ y x \in z$
5		nfvd	$⊢ \neg \forall y y = z \to Ⅎ y φ$
6	4 5	nfand	$⊢ \neg \forall y y = z \to Ⅎ y (x \in z \land φ)$
7	2 6	nfbid	$⊢ \neg \forall y y = z \to Ⅎ y (x \in w \leftrightarrow (x \in z \land φ))$
8	1 7	nfald	$⊢ \neg \forall y y = z \to Ⅎ y \forall x (x \in w \leftrightarrow (x \in z \land φ))$
9		nfvd	$⊢ \neg \forall y y = z \to Ⅎ w \forall x (x \in y \leftrightarrow (x \in z \land φ))$
10		elequ2	$⊢ w = y \to (x \in w \leftrightarrow x \in y)$
11	10	bibi1d	$⊢ w = y \to ((x \in w \leftrightarrow (x \in z \land φ)) \leftrightarrow (x \in y \leftrightarrow (x \in z \land φ)))$
12	11	biimpd	$⊢ w = y \to ((x \in w \leftrightarrow (x \in z \land φ)) \to (x \in y \leftrightarrow (x \in z \land φ)))$
13	12	alimdv	$⊢ w = y \to (\forall x (x \in w \leftrightarrow (x \in z \land φ)) \to \forall x (x \in y \leftrightarrow (x \in z \land φ)))$
14	13	a1i	$⊢ \neg \forall y y = z \to (w = y \to (\forall x (x \in w \leftrightarrow (x \in z \land φ)) \to \forall x (x \in y \leftrightarrow (x \in z \land φ))))$
15		elequ2	$⊢ y = z \to (x \in y \leftrightarrow x \in z)$
16	15	anbi1d	$⊢ y = z \to ((x \in y \land φ) \leftrightarrow (x \in z \land φ))$
17	16	bibi2d	$⊢ y = z \to ((x \in y \leftrightarrow (x \in y \land φ)) \leftrightarrow (x \in y \leftrightarrow (x \in z \land φ)))$
18	17	biimpd	$⊢ y = z \to ((x \in y \leftrightarrow (x \in y \land φ)) \to (x \in y \leftrightarrow (x \in z \land φ)))$
19	18	alimdv	$⊢ y = z \to (\forall x (x \in y \leftrightarrow (x \in y \land φ)) \to \forall x (x \in y \leftrightarrow (x \in z \land φ)))$
20	19	sps	$⊢ \forall y y = z \to (\forall x (x \in y \leftrightarrow (x \in y \land φ)) \to \forall x (x \in y \leftrightarrow (x \in z \land φ)))$
21		ax-sep	$⊢ \exists w \forall x (x \in w \leftrightarrow (x \in z \land φ))$
22		ax-nul	$⊢ \exists y \forall x \neg x \in y$
23		id	$⊢ \neg x \in y \to \neg x \in y$
24	23	bianfd	$⊢ \neg x \in y \to (x \in y \leftrightarrow (x \in y \land φ))$
25	24	alimi	$⊢ \forall x \neg x \in y \to \forall x (x \in y \leftrightarrow (x \in y \land φ))$
26	22 25	eximii	$⊢ \exists y \forall x (x \in y \leftrightarrow (x \in y \land φ))$
27	8 9 14 20 21 26	dvelimexcasei	$⊢ \exists y \forall x (x \in y \leftrightarrow (x \in z \land φ))$

Metamath Proof Explorer

Theorem axsepg3

Proof