axsepgfromrep

Description: A more general version axsepg of the axiom scheme of separation ax-sep derived from the axiom scheme of replacement ax-rep (and first-order logic). The extra generality consists in the absence of a disjoint variable condition on z , ph (that is, variable z may occur in formula ph ). See linked statements for more information. (Contributed by NM, 11-Sep-2006) Remove dependencies on ax-9 to ax-13 . (Revised by SN, 25-Sep-2023) Use ax-sep instead (or axsepg if the extra generality is needed). (New usage is discouraged.)

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

Proof

Step	Hyp	Ref	Expression
1		axrep6	$⊢ \forall w \exists^{*} x (w = x \land φ) \to \exists y \forall x (x \in y \leftrightarrow \exists w \in z (w = x \land φ))$
2		euequ	$⊢ \exists! x x = w$
3	2	eumoi	$⊢ \exists^{*} x x = w$
4		equcomi	$⊢ w = x \to x = w$
5	4	adantr	$⊢ (w = x \land φ) \to x = w$
6	5	moimi	$⊢ \exists^{} x x = w \to \exists^{} x (w = x \land φ)$
7	3 6	ax-mp	$⊢ \exists^{*} x (w = x \land φ)$
8	1 7	mpg	$⊢ \exists y \forall x (x \in y \leftrightarrow \exists w \in z (w = x \land φ))$
9		df-rex	$⊢ \exists w \in z (w = x \land φ) \leftrightarrow \exists w (w \in z \land (w = x \land φ))$
10		an12	$⊢ (w = x \land (w \in z \land φ)) \leftrightarrow (w \in z \land (w = x \land φ))$
11	10	exbii	$⊢ \exists w (w = x \land (w \in z \land φ)) \leftrightarrow \exists w (w \in z \land (w = x \land φ))$
12		elequ1	$⊢ w = x \to (w \in z \leftrightarrow x \in z)$
13	12	anbi1d	$⊢ w = x \to ((w \in z \land φ) \leftrightarrow (x \in z \land φ))$
14	13	equsexvw	$⊢ \exists w (w = x \land (w \in z \land φ)) \leftrightarrow (x \in z \land φ)$
15	9 11 14	3bitr2i	$⊢ \exists w \in z (w = x \land φ) \leftrightarrow (x \in z \land φ)$
16	15	bibi2i	$⊢ (x \in y \leftrightarrow \exists w \in z (w = x \land φ)) \leftrightarrow (x \in y \leftrightarrow (x \in z \land φ))$
17	16	albii	$⊢ \forall x (x \in y \leftrightarrow \exists w \in z (w = x \land φ)) \leftrightarrow \forall x (x \in y \leftrightarrow (x \in z \land φ))$
18	17	exbii	$⊢ \exists y \forall x (x \in y \leftrightarrow \exists w \in z (w = x \land φ)) \leftrightarrow \exists y \forall x (x \in y \leftrightarrow (x \in z \land φ))$
19	8 18	mpbi	$⊢ \exists y \forall x (x \in y \leftrightarrow (x \in z \land φ))$

Metamath Proof Explorer

Theorem axsepgfromrep

Proof