bj-axreprepsep

Description: Strong axiom of replacement (universal closure of ax-rep ) from the axioms of separation and replacement as written in the theorem's hypotheses.

The statement does not require a nonempty universe; most of the proof does not either, except for the use of 19.8a , which could be removed by reworking the proof, since it is applied in a subexpression bound by the variable it introduces. Proof modifications should not introduce steps relying on a nonempty universe, like alrimiv . (Contributed by BJ, 14-Mar-2026) (Proof modification is discouraged.)

	Ref	Expression
Hypotheses	bj-axreprepsep.axsep	$⊢ \forall x \exists s \forall y (y \in s \leftrightarrow (y \in x \land \exists z φ))$
	bj-axreprepsep.axrep	$⊢ \forall s (\forall y \in s \exists! z φ \to \exists t \forall z (z \in t \leftrightarrow \exists y \in s φ))$
Assertion	bj-axreprepsep	$⊢ \forall x (\forall y \in x \exists^{*} z φ \to \exists t \forall z (z \in t \leftrightarrow \exists y \in x φ))$

Proof

Step	Hyp	Ref	Expression
1		bj-axreprepsep.axsep	$⊢ \forall x \exists s \forall y (y \in s \leftrightarrow (y \in x \land \exists z φ))$
2		bj-axreprepsep.axrep	$⊢ \forall s (\forall y \in s \exists! z φ \to \exists t \forall z (z \in t \leftrightarrow \exists y \in s φ))$
3		19.42v	$⊢ \exists s (\forall y \in x \exists^{} z φ \land \forall y (y \in s \leftrightarrow (y \in x \land \exists z φ))) \leftrightarrow (\forall y \in x \exists^{} z φ \land \exists s \forall y (y \in s \leftrightarrow (y \in x \land \exists z φ)))$
4		bianir	$⊢ (\exists t \forall z (z \in t \leftrightarrow \exists y \in s φ) \land (\exists t \forall z (z \in t \leftrightarrow \exists y \in x φ) \leftrightarrow \exists t \forall z (z \in t \leftrightarrow \exists y \in s φ))) \to \exists t \forall z (z \in t \leftrightarrow \exists y \in x φ)$
5	4	ax-gen	$⊢ \forall s ((\exists t \forall z (z \in t \leftrightarrow \exists y \in s φ) \land (\exists t \forall z (z \in t \leftrightarrow \exists y \in x φ) \leftrightarrow \exists t \forall z (z \in t \leftrightarrow \exists y \in s φ))) \to \exists t \forall z (z \in t \leftrightarrow \exists y \in x φ))$
6		pm3.43	$⊢ (((\forall y \in x \exists^{} z φ \land \forall y (y \in s \leftrightarrow (y \in x \land \exists z φ))) \to \exists t \forall z (z \in t \leftrightarrow \exists y \in s φ)) \land ((\forall y \in x \exists^{} z φ \land \forall y (y \in s \leftrightarrow (y \in x \land \exists z φ))) \to (\exists t \forall z (z \in t \leftrightarrow \exists y \in x φ) \leftrightarrow \exists t \forall z (z \in t \leftrightarrow \exists y \in s φ)))) \to ((\forall y \in x \exists^{*} z φ \land \forall y (y \in s \leftrightarrow (y \in x \land \exists z φ))) \to (\exists t \forall z (z \in t \leftrightarrow \exists y \in s φ) \land (\exists t \forall z (z \in t \leftrightarrow \exists y \in x φ) \leftrightarrow \exists t \forall z (z \in t \leftrightarrow \exists y \in s φ))))$
7		df-ral	$⊢ \forall y \in x \exists^{} z φ \leftrightarrow \forall y (y \in x \to \exists^{} z φ)$
8		bicom1	$⊢ (y \in s \leftrightarrow (y \in x \land \exists z φ)) \to ((y \in x \land \exists z φ) \leftrightarrow y \in s)$
9	8	biimprcd	$⊢ y \in s \to ((y \in s \leftrightarrow (y \in x \land \exists z φ)) \to (y \in x \land \exists z φ))$
10		df-eu	$⊢ \exists! z φ \leftrightarrow (\exists z φ \land \exists^{*} z φ)$
11	10	simplbi2com	$⊢ \exists^{*} z φ \to (\exists z φ \to \exists! z φ)$
12	11	imim2i	$⊢ (y \in x \to \exists^{*} z φ) \to (y \in x \to (\exists z φ \to \exists! z φ))$
13	12	impd	$⊢ (y \in x \to \exists^{*} z φ) \to ((y \in x \land \exists z φ) \to \exists! z φ)$
14	13	com12	$⊢ (y \in x \land \exists z φ) \to ((y \in x \to \exists^{*} z φ) \to \exists! z φ)$
15	9 14	syl6	$⊢ y \in s \to ((y \in s \leftrightarrow (y \in x \land \exists z φ)) \to ((y \in x \to \exists^{*} z φ) \to \exists! z φ))$
16	15	impd	$⊢ y \in s \to (((y \in s \leftrightarrow (y \in x \land \exists z φ)) \land (y \in x \to \exists^{*} z φ)) \to \exists! z φ)$
17	16	com12	$⊢ ((y \in s \leftrightarrow (y \in x \land \exists z φ)) \land (y \in x \to \exists^{*} z φ)) \to (y \in s \to \exists! z φ)$
18	17	ancoms	$⊢ ((y \in x \to \exists^{*} z φ) \land (y \in s \leftrightarrow (y \in x \land \exists z φ))) \to (y \in s \to \exists! z φ)$
19	18	alanimi	$⊢ (\forall y (y \in x \to \exists^{*} z φ) \land \forall y (y \in s \leftrightarrow (y \in x \land \exists z φ))) \to \forall y (y \in s \to \exists! z φ)$
20	7 19	sylanb	$⊢ (\forall y \in x \exists^{*} z φ \land \forall y (y \in s \leftrightarrow (y \in x \land \exists z φ))) \to \forall y (y \in s \to \exists! z φ)$
21	20	ralrid	$⊢ (\forall y \in x \exists^{*} z φ \land \forall y (y \in s \leftrightarrow (y \in x \land \exists z φ))) \to \forall y \in s \exists! z φ$
22	21	ax-gen	$⊢ \forall s ((\forall y \in x \exists^{*} z φ \land \forall y (y \in s \leftrightarrow (y \in x \land \exists z φ))) \to \forall y \in s \exists! z φ)$
23	2 22	barbara	$⊢ \forall s ((\forall y \in x \exists^{*} z φ \land \forall y (y \in s \leftrightarrow (y \in x \land \exists z φ))) \to \exists t \forall z (z \in t \leftrightarrow \exists y \in s φ))$
24		nfv	$⊢ Ⅎ z y \in s$
25		nfv	$⊢ Ⅎ z y \in x$
26		nfe1	$⊢ Ⅎ z \exists z φ$
27	25 26	nfan	$⊢ Ⅎ z (y \in x \land \exists z φ)$
28	24 27	nfbi	$⊢ Ⅎ z (y \in s \leftrightarrow (y \in x \land \exists z φ))$
29	28	nfal	$⊢ Ⅎ z \forall y (y \in s \leftrightarrow (y \in x \land \exists z φ))$
30		19.8a	$⊢ φ \to \exists z φ$
31		biimpr	$⊢ (y \in s \leftrightarrow (y \in x \land \exists z φ)) \to ((y \in x \land \exists z φ) \to y \in s)$
32	30 31	sylan2i	$⊢ (y \in s \leftrightarrow (y \in x \land \exists z φ)) \to ((y \in x \land φ) \to y \in s)$
33		simpr	$⊢ (y \in x \land φ) \to φ$
34	32 33	jca2	$⊢ (y \in s \leftrightarrow (y \in x \land \exists z φ)) \to ((y \in x \land φ) \to (y \in s \land φ))$
35		bj-bisimpl	$⊢ (y \in s \leftrightarrow (y \in x \land \exists z φ)) \to (y \in s \to y \in x)$
36	35	anim1d	$⊢ (y \in s \leftrightarrow (y \in x \land \exists z φ)) \to ((y \in s \land φ) \to (y \in x \land φ))$
37	34 36	impbid	$⊢ (y \in s \leftrightarrow (y \in x \land \exists z φ)) \to ((y \in x \land φ) \leftrightarrow (y \in s \land φ))$
38	37	alexbii	$⊢ \forall y (y \in s \leftrightarrow (y \in x \land \exists z φ)) \to (\exists y (y \in x \land φ) \leftrightarrow \exists y (y \in s \land φ))$
39		df-rex	$⊢ \exists y \in x φ \leftrightarrow \exists y (y \in x \land φ)$
40		df-rex	$⊢ \exists y \in s φ \leftrightarrow \exists y (y \in s \land φ)$
41	38 39 40	3bitr4g	$⊢ \forall y (y \in s \leftrightarrow (y \in x \land \exists z φ)) \to (\exists y \in x φ \leftrightarrow \exists y \in s φ)$
42	41	bibi2d	$⊢ \forall y (y \in s \leftrightarrow (y \in x \land \exists z φ)) \to ((z \in t \leftrightarrow \exists y \in x φ) \leftrightarrow (z \in t \leftrightarrow \exists y \in s φ))$
43	29 42	albid	$⊢ \forall y (y \in s \leftrightarrow (y \in x \land \exists z φ)) \to (\forall z (z \in t \leftrightarrow \exists y \in x φ) \leftrightarrow \forall z (z \in t \leftrightarrow \exists y \in s φ))$
44	43	exbidv	$⊢ \forall y (y \in s \leftrightarrow (y \in x \land \exists z φ)) \to (\exists t \forall z (z \in t \leftrightarrow \exists y \in x φ) \leftrightarrow \exists t \forall z (z \in t \leftrightarrow \exists y \in s φ))$
45	44	adantl	$⊢ (\forall y \in x \exists^{*} z φ \land \forall y (y \in s \leftrightarrow (y \in x \land \exists z φ))) \to (\exists t \forall z (z \in t \leftrightarrow \exists y \in x φ) \leftrightarrow \exists t \forall z (z \in t \leftrightarrow \exists y \in s φ))$
46	45	ax-gen	$⊢ \forall s ((\forall y \in x \exists^{*} z φ \land \forall y (y \in s \leftrightarrow (y \in x \land \exists z φ))) \to (\exists t \forall z (z \in t \leftrightarrow \exists y \in x φ) \leftrightarrow \exists t \forall z (z \in t \leftrightarrow \exists y \in s φ)))$
47		19.26	$⊢ \forall s (((\forall y \in x \exists^{} z φ \land \forall y (y \in s \leftrightarrow (y \in x \land \exists z φ))) \to \exists t \forall z (z \in t \leftrightarrow \exists y \in s φ)) \land ((\forall y \in x \exists^{} z φ \land \forall y (y \in s \leftrightarrow (y \in x \land \exists z φ))) \to (\exists t \forall z (z \in t \leftrightarrow \exists y \in x φ) \leftrightarrow \exists t \forall z (z \in t \leftrightarrow \exists y \in s φ)))) \leftrightarrow (\forall s ((\forall y \in x \exists^{} z φ \land \forall y (y \in s \leftrightarrow (y \in x \land \exists z φ))) \to \exists t \forall z (z \in t \leftrightarrow \exists y \in s φ)) \land \forall s ((\forall y \in x \exists^{} z φ \land \forall y (y \in s \leftrightarrow (y \in x \land \exists z φ))) \to (\exists t \forall z (z \in t \leftrightarrow \exists y \in x φ) \leftrightarrow \exists t \forall z (z \in t \leftrightarrow \exists y \in s φ))))$
48	23 46 47	mpbir2an	$⊢ \forall s (((\forall y \in x \exists^{} z φ \land \forall y (y \in s \leftrightarrow (y \in x \land \exists z φ))) \to \exists t \forall z (z \in t \leftrightarrow \exists y \in s φ)) \land ((\forall y \in x \exists^{} z φ \land \forall y (y \in s \leftrightarrow (y \in x \land \exists z φ))) \to (\exists t \forall z (z \in t \leftrightarrow \exists y \in x φ) \leftrightarrow \exists t \forall z (z \in t \leftrightarrow \exists y \in s φ))))$
49	6 48	bj-alimii	$⊢ \forall s ((\forall y \in x \exists^{*} z φ \land \forall y (y \in s \leftrightarrow (y \in x \land \exists z φ))) \to (\exists t \forall z (z \in t \leftrightarrow \exists y \in s φ) \land (\exists t \forall z (z \in t \leftrightarrow \exists y \in x φ) \leftrightarrow \exists t \forall z (z \in t \leftrightarrow \exists y \in s φ))))$
50	5 49	barbara	$⊢ \forall s ((\forall y \in x \exists^{*} z φ \land \forall y (y \in s \leftrightarrow (y \in x \land \exists z φ))) \to \exists t \forall z (z \in t \leftrightarrow \exists y \in x φ))$
51		exim	$⊢ \forall s ((\forall y \in x \exists^{} z φ \land \forall y (y \in s \leftrightarrow (y \in x \land \exists z φ))) \to \exists t \forall z (z \in t \leftrightarrow \exists y \in x φ)) \to (\exists s (\forall y \in x \exists^{} z φ \land \forall y (y \in s \leftrightarrow (y \in x \land \exists z φ))) \to \exists s \exists t \forall z (z \in t \leftrightarrow \exists y \in x φ))$
52	50 51	ax-mp	$⊢ \exists s (\forall y \in x \exists^{*} z φ \land \forall y (y \in s \leftrightarrow (y \in x \land \exists z φ))) \to \exists s \exists t \forall z (z \in t \leftrightarrow \exists y \in x φ)$
53	3 52	sylbir	$⊢ (\forall y \in x \exists^{*} z φ \land \exists s \forall y (y \in s \leftrightarrow (y \in x \land \exists z φ))) \to \exists s \exists t \forall z (z \in t \leftrightarrow \exists y \in x φ)$
54	53	ex	$⊢ \forall y \in x \exists^{*} z φ \to (\exists s \forall y (y \in s \leftrightarrow (y \in x \land \exists z φ)) \to \exists s \exists t \forall z (z \in t \leftrightarrow \exists y \in x φ))$
55		ax5e	$⊢ \exists s \exists t \forall z (z \in t \leftrightarrow \exists y \in x φ) \to \exists t \forall z (z \in t \leftrightarrow \exists y \in x φ)$
56	54 55	syl6	$⊢ \forall y \in x \exists^{*} z φ \to (\exists s \forall y (y \in s \leftrightarrow (y \in x \land \exists z φ)) \to \exists t \forall z (z \in t \leftrightarrow \exists y \in x φ))$
57	56 1	bj-almpig	$⊢ \forall x (\forall y \in x \exists^{*} z φ \to \exists t \forall z (z \in t \leftrightarrow \exists y \in x φ))$

Metamath Proof Explorer

Theorem bj-axreprepsep

Proof