axrep6

Description: A condensed form of ax-rep . (Contributed by SN, 18-Sep-2023) (Proof shortened by Matthew House, 18-Sep-2025)

		Ref	Expression
	Assertion	axrep6	$⊢ \forall w \exists^{*} z φ \to \exists y \forall z (z \in y \leftrightarrow \exists w \in x φ)$

Step	Hyp	Ref	Expression
1		axrep4v	$⊢ \forall w \exists y \forall z (φ \to z = y) \to \exists y \forall z (z \in y \leftrightarrow \exists w (w \in x \land φ))$
2		df-mo	$⊢ \exists^{*} z φ \leftrightarrow \exists y \forall z (φ \to z = y)$
3	2	albii	$⊢ \forall w \exists^{*} z φ \leftrightarrow \forall w \exists y \forall z (φ \to z = y)$
4		df-rex	$⊢ \exists w \in x φ \leftrightarrow \exists w (w \in x \land φ)$
5	4	bibi2i	$⊢ (z \in y \leftrightarrow \exists w \in x φ) \leftrightarrow (z \in y \leftrightarrow \exists w (w \in x \land φ))$
6	5	albii	$⊢ \forall z (z \in y \leftrightarrow \exists w \in x φ) \leftrightarrow \forall z (z \in y \leftrightarrow \exists w (w \in x \land φ))$
7	6	exbii	$⊢ \exists y \forall z (z \in y \leftrightarrow \exists w \in x φ) \leftrightarrow \exists y \forall z (z \in y \leftrightarrow \exists w (w \in x \land φ))$
8	1 3 7	3imtr4i	$⊢ \forall w \exists^{*} z φ \to \exists y \forall z (z \in y \leftrightarrow \exists w \in x φ)$

Metamath Proof Explorer