Theorem bj-axreprepsep 37314

Description: Strong axiom of replacement (universal closure of ax-rep 5226) 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 2189, 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 1929. (Contributed by BJ, 14-Mar-2026.) (Proof modification is discouraged.)

Hypotheses

Ref	Expression
bj-axreprepsep.axsep	⊢ ∀𝑥∃𝑠∀𝑦(𝑦 ∈ 𝑠 ↔ (𝑦 ∈ 𝑥 ∧ ∃𝑧𝜑))
bj-axreprepsep.axrep	⊢ ∀𝑠(∀𝑦 ∈ 𝑠 ∃!𝑧𝜑 → ∃𝑡∀𝑧(𝑧 ∈ 𝑡 ↔ ∃𝑦 ∈ 𝑠 𝜑))

Assertion

Ref	Expression
bj-axreprepsep	⊢ ∀𝑥(∀𝑦 ∈ 𝑥 ∃*𝑧𝜑 → ∃𝑡∀𝑧(𝑧 ∈ 𝑡 ↔ ∃𝑦 ∈ 𝑥 𝜑))

Distinct variable groups:   𝑡,𝑠,𝑥,𝑦,𝑧   𝜑,𝑠,𝑡,𝑥,𝑦

Allowed substitution hint:   𝜑(𝑧)

Proof of Theorem bj-axreprepsep

Step	Hyp	Ref	Expression
1		19.42v 1955	. . . . 5 ⊢ (∃𝑠(∀𝑦 ∈ 𝑥 ∃*𝑧𝜑 ∧ ∀𝑦(𝑦 ∈ 𝑠 ↔ (𝑦 ∈ 𝑥 ∧ ∃𝑧𝜑))) ↔ (∀𝑦 ∈ 𝑥 ∃*𝑧𝜑 ∧ ∃𝑠∀𝑦(𝑦 ∈ 𝑠 ↔ (𝑦 ∈ 𝑥 ∧ ∃𝑧𝜑))))
2		bianir 1059	. . . . . . . 8 ⊢ ((∃𝑡∀𝑧(𝑧 ∈ 𝑡 ↔ ∃𝑦 ∈ 𝑠 𝜑) ∧ (∃𝑡∀𝑧(𝑧 ∈ 𝑡 ↔ ∃𝑦 ∈ 𝑥 𝜑) ↔ ∃𝑡∀𝑧(𝑧 ∈ 𝑡 ↔ ∃𝑦 ∈ 𝑠 𝜑))) → ∃𝑡∀𝑧(𝑧 ∈ 𝑡 ↔ ∃𝑦 ∈ 𝑥 𝜑))
3	2	ax-gen 1797	. . . . . . 7 ⊢ ∀𝑠((∃𝑡∀𝑧(𝑧 ∈ 𝑡 ↔ ∃𝑦 ∈ 𝑠 𝜑) ∧ (∃𝑡∀𝑧(𝑧 ∈ 𝑡 ↔ ∃𝑦 ∈ 𝑥 𝜑) ↔ ∃𝑡∀𝑧(𝑧 ∈ 𝑡 ↔ ∃𝑦 ∈ 𝑠 𝜑))) → ∃𝑡∀𝑧(𝑧 ∈ 𝑡 ↔ ∃𝑦 ∈ 𝑥 𝜑))
4		pm3.43 473	. . . . . . . 8 ⊢ ((((∀𝑦 ∈ 𝑥 ∃*𝑧𝜑 ∧ ∀𝑦(𝑦 ∈ 𝑠 ↔ (𝑦 ∈ 𝑥 ∧ ∃𝑧𝜑))) → ∃𝑡∀𝑧(𝑧 ∈ 𝑡 ↔ ∃𝑦 ∈ 𝑠 𝜑)) ∧ ((∀𝑦 ∈ 𝑥 ∃*𝑧𝜑 ∧ ∀𝑦(𝑦 ∈ 𝑠 ↔ (𝑦 ∈ 𝑥 ∧ ∃𝑧𝜑))) → (∃𝑡∀𝑧(𝑧 ∈ 𝑡 ↔ ∃𝑦 ∈ 𝑥 𝜑) ↔ ∃𝑡∀𝑧(𝑧 ∈ 𝑡 ↔ ∃𝑦 ∈ 𝑠 𝜑)))) → ((∀𝑦 ∈ 𝑥 ∃*𝑧𝜑 ∧ ∀𝑦(𝑦 ∈ 𝑠 ↔ (𝑦 ∈ 𝑥 ∧ ∃𝑧𝜑))) → (∃𝑡∀𝑧(𝑧 ∈ 𝑡 ↔ ∃𝑦 ∈ 𝑠 𝜑) ∧ (∃𝑡∀𝑧(𝑧 ∈ 𝑡 ↔ ∃𝑦 ∈ 𝑥 𝜑) ↔ ∃𝑡∀𝑧(𝑧 ∈ 𝑡 ↔ ∃𝑦 ∈ 𝑠 𝜑)))))
5		bj-axreprepsep.axrep	. . . . . . . . . 10 ⊢ ∀𝑠(∀𝑦 ∈ 𝑠 ∃!𝑧𝜑 → ∃𝑡∀𝑧(𝑧 ∈ 𝑡 ↔ ∃𝑦 ∈ 𝑠 𝜑))
6		df-ral 3053	. . . . . . . . . . . . 13 ⊢ (∀𝑦 ∈ 𝑥 ∃*𝑧𝜑 ↔ ∀𝑦(𝑦 ∈ 𝑥 → ∃*𝑧𝜑))
7		bicom1 221	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑦 ∈ 𝑠 ↔ (𝑦 ∈ 𝑥 ∧ ∃𝑧𝜑)) → ((𝑦 ∈ 𝑥 ∧ ∃𝑧𝜑) ↔ 𝑦 ∈ 𝑠))
8	7	biimprcd 250	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑦 ∈ 𝑠 → ((𝑦 ∈ 𝑠 ↔ (𝑦 ∈ 𝑥 ∧ ∃𝑧𝜑)) → (𝑦 ∈ 𝑥 ∧ ∃𝑧𝜑)))
9		df-eu 2570	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (∃!𝑧𝜑 ↔ (∃𝑧𝜑 ∧ ∃*𝑧𝜑))
10	9	simplbi2com 502	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (∃*𝑧𝜑 → (∃𝑧𝜑 → ∃!𝑧𝜑))
11	10	imim2i 16	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑦 ∈ 𝑥 → ∃*𝑧𝜑) → (𝑦 ∈ 𝑥 → (∃𝑧𝜑 → ∃!𝑧𝜑)))
12	11	impd 410	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑦 ∈ 𝑥 → ∃*𝑧𝜑) → ((𝑦 ∈ 𝑥 ∧ ∃𝑧𝜑) → ∃!𝑧𝜑))
13	12	com12 32	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑦 ∈ 𝑥 ∧ ∃𝑧𝜑) → ((𝑦 ∈ 𝑥 → ∃*𝑧𝜑) → ∃!𝑧𝜑))
14	8, 13	syl6 35	. . . . . . . . . . . . . . . . 17 ⊢ (𝑦 ∈ 𝑠 → ((𝑦 ∈ 𝑠 ↔ (𝑦 ∈ 𝑥 ∧ ∃𝑧𝜑)) → ((𝑦 ∈ 𝑥 → ∃*𝑧𝜑) → ∃!𝑧𝜑)))
15	14	impd 410	. . . . . . . . . . . . . . . 16 ⊢ (𝑦 ∈ 𝑠 → (((𝑦 ∈ 𝑠 ↔ (𝑦 ∈ 𝑥 ∧ ∃𝑧𝜑)) ∧ (𝑦 ∈ 𝑥 → ∃*𝑧𝜑)) → ∃!𝑧𝜑))
16	15	com12 32	. . . . . . . . . . . . . . 15 ⊢ (((𝑦 ∈ 𝑠 ↔ (𝑦 ∈ 𝑥 ∧ ∃𝑧𝜑)) ∧ (𝑦 ∈ 𝑥 → ∃*𝑧𝜑)) → (𝑦 ∈ 𝑠 → ∃!𝑧𝜑))
17	16	ancoms 458	. . . . . . . . . . . . . 14 ⊢ (((𝑦 ∈ 𝑥 → ∃*𝑧𝜑) ∧ (𝑦 ∈ 𝑠 ↔ (𝑦 ∈ 𝑥 ∧ ∃𝑧𝜑))) → (𝑦 ∈ 𝑠 → ∃!𝑧𝜑))
18	17	alanimi 1818	. . . . . . . . . . . . 13 ⊢ ((∀𝑦(𝑦 ∈ 𝑥 → ∃*𝑧𝜑) ∧ ∀𝑦(𝑦 ∈ 𝑠 ↔ (𝑦 ∈ 𝑥 ∧ ∃𝑧𝜑))) → ∀𝑦(𝑦 ∈ 𝑠 → ∃!𝑧𝜑))
19	6, 18	sylanb 582	. . . . . . . . . . . 12 ⊢ ((∀𝑦 ∈ 𝑥 ∃*𝑧𝜑 ∧ ∀𝑦(𝑦 ∈ 𝑠 ↔ (𝑦 ∈ 𝑥 ∧ ∃𝑧𝜑))) → ∀𝑦(𝑦 ∈ 𝑠 → ∃!𝑧𝜑))
20	19	ralrid 3060	. . . . . . . . . . 11 ⊢ ((∀𝑦 ∈ 𝑥 ∃*𝑧𝜑 ∧ ∀𝑦(𝑦 ∈ 𝑠 ↔ (𝑦 ∈ 𝑥 ∧ ∃𝑧𝜑))) → ∀𝑦 ∈ 𝑠 ∃!𝑧𝜑)
21	20	ax-gen 1797	. . . . . . . . . 10 ⊢ ∀𝑠((∀𝑦 ∈ 𝑥 ∃*𝑧𝜑 ∧ ∀𝑦(𝑦 ∈ 𝑠 ↔ (𝑦 ∈ 𝑥 ∧ ∃𝑧𝜑))) → ∀𝑦 ∈ 𝑠 ∃!𝑧𝜑)
22	5, 21	barbara 2664	. . . . . . . . 9 ⊢ ∀𝑠((∀𝑦 ∈ 𝑥 ∃*𝑧𝜑 ∧ ∀𝑦(𝑦 ∈ 𝑠 ↔ (𝑦 ∈ 𝑥 ∧ ∃𝑧𝜑))) → ∃𝑡∀𝑧(𝑧 ∈ 𝑡 ↔ ∃𝑦 ∈ 𝑠 𝜑))
23		nfv 1916	. . . . . . . . . . . . . . 15 ⊢ Ⅎ𝑧 𝑦 ∈ 𝑠
24		nfv 1916	. . . . . . . . . . . . . . . 16 ⊢ Ⅎ𝑧 𝑦 ∈ 𝑥
25		nfe1 2156	. . . . . . . . . . . . . . . 16 ⊢ Ⅎ𝑧∃𝑧𝜑
26	24, 25	nfan 1901	. . . . . . . . . . . . . . 15 ⊢ Ⅎ𝑧(𝑦 ∈ 𝑥 ∧ ∃𝑧𝜑)
27	23, 26	nfbi 1905	. . . . . . . . . . . . . 14 ⊢ Ⅎ𝑧(𝑦 ∈ 𝑠 ↔ (𝑦 ∈ 𝑥 ∧ ∃𝑧𝜑))
28	27	nfal 2329	. . . . . . . . . . . . 13 ⊢ Ⅎ𝑧∀𝑦(𝑦 ∈ 𝑠 ↔ (𝑦 ∈ 𝑥 ∧ ∃𝑧𝜑))
29		19.8a 2189	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → ∃𝑧𝜑)
30		biimpr 220	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑦 ∈ 𝑠 ↔ (𝑦 ∈ 𝑥 ∧ ∃𝑧𝜑)) → ((𝑦 ∈ 𝑥 ∧ ∃𝑧𝜑) → 𝑦 ∈ 𝑠))
31	29, 30	sylan2i 607	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑦 ∈ 𝑠 ↔ (𝑦 ∈ 𝑥 ∧ ∃𝑧𝜑)) → ((𝑦 ∈ 𝑥 ∧ 𝜑) → 𝑦 ∈ 𝑠))
32		simpr 484	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑦 ∈ 𝑥 ∧ 𝜑) → 𝜑)
33	31, 32	jca2 513	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑦 ∈ 𝑠 ↔ (𝑦 ∈ 𝑥 ∧ ∃𝑧𝜑)) → ((𝑦 ∈ 𝑥 ∧ 𝜑) → (𝑦 ∈ 𝑠 ∧ 𝜑)))
34		bj-bisimpl 36774	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑦 ∈ 𝑠 ↔ (𝑦 ∈ 𝑥 ∧ ∃𝑧𝜑)) → (𝑦 ∈ 𝑠 → 𝑦 ∈ 𝑥))
35	34	anim1d 612	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑦 ∈ 𝑠 ↔ (𝑦 ∈ 𝑥 ∧ ∃𝑧𝜑)) → ((𝑦 ∈ 𝑠 ∧ 𝜑) → (𝑦 ∈ 𝑥 ∧ 𝜑)))
36	33, 35	impbid 212	. . . . . . . . . . . . . . . 16 ⊢ ((𝑦 ∈ 𝑠 ↔ (𝑦 ∈ 𝑥 ∧ ∃𝑧𝜑)) → ((𝑦 ∈ 𝑥 ∧ 𝜑) ↔ (𝑦 ∈ 𝑠 ∧ 𝜑)))
37	36	alexbii 1835	. . . . . . . . . . . . . . 15 ⊢ (∀𝑦(𝑦 ∈ 𝑠 ↔ (𝑦 ∈ 𝑥 ∧ ∃𝑧𝜑)) → (∃𝑦(𝑦 ∈ 𝑥 ∧ 𝜑) ↔ ∃𝑦(𝑦 ∈ 𝑠 ∧ 𝜑)))
38		df-rex 3063	. . . . . . . . . . . . . . 15 ⊢ (∃𝑦 ∈ 𝑥 𝜑 ↔ ∃𝑦(𝑦 ∈ 𝑥 ∧ 𝜑))
39		df-rex 3063	. . . . . . . . . . . . . . 15 ⊢ (∃𝑦 ∈ 𝑠 𝜑 ↔ ∃𝑦(𝑦 ∈ 𝑠 ∧ 𝜑))
40	37, 38, 39	3bitr4g 314	. . . . . . . . . . . . . 14 ⊢ (∀𝑦(𝑦 ∈ 𝑠 ↔ (𝑦 ∈ 𝑥 ∧ ∃𝑧𝜑)) → (∃𝑦 ∈ 𝑥 𝜑 ↔ ∃𝑦 ∈ 𝑠 𝜑))
41	40	bibi2d 342	. . . . . . . . . . . . 13 ⊢ (∀𝑦(𝑦 ∈ 𝑠 ↔ (𝑦 ∈ 𝑥 ∧ ∃𝑧𝜑)) → ((𝑧 ∈ 𝑡 ↔ ∃𝑦 ∈ 𝑥 𝜑) ↔ (𝑧 ∈ 𝑡 ↔ ∃𝑦 ∈ 𝑠 𝜑)))
42	28, 41	albid 2230	. . . . . . . . . . . 12 ⊢ (∀𝑦(𝑦 ∈ 𝑠 ↔ (𝑦 ∈ 𝑥 ∧ ∃𝑧𝜑)) → (∀𝑧(𝑧 ∈ 𝑡 ↔ ∃𝑦 ∈ 𝑥 𝜑) ↔ ∀𝑧(𝑧 ∈ 𝑡 ↔ ∃𝑦 ∈ 𝑠 𝜑)))
43	42	exbidv 1923	. . . . . . . . . . 11 ⊢ (∀𝑦(𝑦 ∈ 𝑠 ↔ (𝑦 ∈ 𝑥 ∧ ∃𝑧𝜑)) → (∃𝑡∀𝑧(𝑧 ∈ 𝑡 ↔ ∃𝑦 ∈ 𝑥 𝜑) ↔ ∃𝑡∀𝑧(𝑧 ∈ 𝑡 ↔ ∃𝑦 ∈ 𝑠 𝜑)))
44	43	adantl 481	. . . . . . . . . 10 ⊢ ((∀𝑦 ∈ 𝑥 ∃*𝑧𝜑 ∧ ∀𝑦(𝑦 ∈ 𝑠 ↔ (𝑦 ∈ 𝑥 ∧ ∃𝑧𝜑))) → (∃𝑡∀𝑧(𝑧 ∈ 𝑡 ↔ ∃𝑦 ∈ 𝑥 𝜑) ↔ ∃𝑡∀𝑧(𝑧 ∈ 𝑡 ↔ ∃𝑦 ∈ 𝑠 𝜑)))
45	44	ax-gen 1797	. . . . . . . . 9 ⊢ ∀𝑠((∀𝑦 ∈ 𝑥 ∃*𝑧𝜑 ∧ ∀𝑦(𝑦 ∈ 𝑠 ↔ (𝑦 ∈ 𝑥 ∧ ∃𝑧𝜑))) → (∃𝑡∀𝑧(𝑧 ∈ 𝑡 ↔ ∃𝑦 ∈ 𝑥 𝜑) ↔ ∃𝑡∀𝑧(𝑧 ∈ 𝑡 ↔ ∃𝑦 ∈ 𝑠 𝜑)))
46		19.26 1872	. . . . . . . . 9 ⊢ (∀𝑠(((∀𝑦 ∈ 𝑥 ∃*𝑧𝜑 ∧ ∀𝑦(𝑦 ∈ 𝑠 ↔ (𝑦 ∈ 𝑥 ∧ ∃𝑧𝜑))) → ∃𝑡∀𝑧(𝑧 ∈ 𝑡 ↔ ∃𝑦 ∈ 𝑠 𝜑)) ∧ ((∀𝑦 ∈ 𝑥 ∃*𝑧𝜑 ∧ ∀𝑦(𝑦 ∈ 𝑠 ↔ (𝑦 ∈ 𝑥 ∧ ∃𝑧𝜑))) → (∃𝑡∀𝑧(𝑧 ∈ 𝑡 ↔ ∃𝑦 ∈ 𝑥 𝜑) ↔ ∃𝑡∀𝑧(𝑧 ∈ 𝑡 ↔ ∃𝑦 ∈ 𝑠 𝜑)))) ↔ (∀𝑠((∀𝑦 ∈ 𝑥 ∃*𝑧𝜑 ∧ ∀𝑦(𝑦 ∈ 𝑠 ↔ (𝑦 ∈ 𝑥 ∧ ∃𝑧𝜑))) → ∃𝑡∀𝑧(𝑧 ∈ 𝑡 ↔ ∃𝑦 ∈ 𝑠 𝜑)) ∧ ∀𝑠((∀𝑦 ∈ 𝑥 ∃*𝑧𝜑 ∧ ∀𝑦(𝑦 ∈ 𝑠 ↔ (𝑦 ∈ 𝑥 ∧ ∃𝑧𝜑))) → (∃𝑡∀𝑧(𝑧 ∈ 𝑡 ↔ ∃𝑦 ∈ 𝑥 𝜑) ↔ ∃𝑡∀𝑧(𝑧 ∈ 𝑡 ↔ ∃𝑦 ∈ 𝑠 𝜑)))))
47	22, 45, 46	mpbir2an 712	. . . . . . . 8 ⊢ ∀𝑠(((∀𝑦 ∈ 𝑥 ∃*𝑧𝜑 ∧ ∀𝑦(𝑦 ∈ 𝑠 ↔ (𝑦 ∈ 𝑥 ∧ ∃𝑧𝜑))) → ∃𝑡∀𝑧(𝑧 ∈ 𝑡 ↔ ∃𝑦 ∈ 𝑠 𝜑)) ∧ ((∀𝑦 ∈ 𝑥 ∃*𝑧𝜑 ∧ ∀𝑦(𝑦 ∈ 𝑠 ↔ (𝑦 ∈ 𝑥 ∧ ∃𝑧𝜑))) → (∃𝑡∀𝑧(𝑧 ∈ 𝑡 ↔ ∃𝑦 ∈ 𝑥 𝜑) ↔ ∃𝑡∀𝑧(𝑧 ∈ 𝑡 ↔ ∃𝑦 ∈ 𝑠 𝜑))))
48	4, 47	bj-alimii 36833	. . . . . . 7 ⊢ ∀𝑠((∀𝑦 ∈ 𝑥 ∃*𝑧𝜑 ∧ ∀𝑦(𝑦 ∈ 𝑠 ↔ (𝑦 ∈ 𝑥 ∧ ∃𝑧𝜑))) → (∃𝑡∀𝑧(𝑧 ∈ 𝑡 ↔ ∃𝑦 ∈ 𝑠 𝜑) ∧ (∃𝑡∀𝑧(𝑧 ∈ 𝑡 ↔ ∃𝑦 ∈ 𝑥 𝜑) ↔ ∃𝑡∀𝑧(𝑧 ∈ 𝑡 ↔ ∃𝑦 ∈ 𝑠 𝜑))))
49	3, 48	barbara 2664	. . . . . 6 ⊢ ∀𝑠((∀𝑦 ∈ 𝑥 ∃*𝑧𝜑 ∧ ∀𝑦(𝑦 ∈ 𝑠 ↔ (𝑦 ∈ 𝑥 ∧ ∃𝑧𝜑))) → ∃𝑡∀𝑧(𝑧 ∈ 𝑡 ↔ ∃𝑦 ∈ 𝑥 𝜑))
50		exim 1836	. . . . . 6 ⊢ (∀𝑠((∀𝑦 ∈ 𝑥 ∃*𝑧𝜑 ∧ ∀𝑦(𝑦 ∈ 𝑠 ↔ (𝑦 ∈ 𝑥 ∧ ∃𝑧𝜑))) → ∃𝑡∀𝑧(𝑧 ∈ 𝑡 ↔ ∃𝑦 ∈ 𝑥 𝜑)) → (∃𝑠(∀𝑦 ∈ 𝑥 ∃*𝑧𝜑 ∧ ∀𝑦(𝑦 ∈ 𝑠 ↔ (𝑦 ∈ 𝑥 ∧ ∃𝑧𝜑))) → ∃𝑠∃𝑡∀𝑧(𝑧 ∈ 𝑡 ↔ ∃𝑦 ∈ 𝑥 𝜑)))
51	49, 50	ax-mp 5	. . . . 5 ⊢ (∃𝑠(∀𝑦 ∈ 𝑥 ∃*𝑧𝜑 ∧ ∀𝑦(𝑦 ∈ 𝑠 ↔ (𝑦 ∈ 𝑥 ∧ ∃𝑧𝜑))) → ∃𝑠∃𝑡∀𝑧(𝑧 ∈ 𝑡 ↔ ∃𝑦 ∈ 𝑥 𝜑))
52	1, 51	sylbir 235	. . . 4 ⊢ ((∀𝑦 ∈ 𝑥 ∃*𝑧𝜑 ∧ ∃𝑠∀𝑦(𝑦 ∈ 𝑠 ↔ (𝑦 ∈ 𝑥 ∧ ∃𝑧𝜑))) → ∃𝑠∃𝑡∀𝑧(𝑧 ∈ 𝑡 ↔ ∃𝑦 ∈ 𝑥 𝜑))
53	52	ex 412	. . 3 ⊢ (∀𝑦 ∈ 𝑥 ∃*𝑧𝜑 → (∃𝑠∀𝑦(𝑦 ∈ 𝑠 ↔ (𝑦 ∈ 𝑥 ∧ ∃𝑧𝜑)) → ∃𝑠∃𝑡∀𝑧(𝑧 ∈ 𝑡 ↔ ∃𝑦 ∈ 𝑥 𝜑)))
54		ax5e 1914	. . 3 ⊢ (∃𝑠∃𝑡∀𝑧(𝑧 ∈ 𝑡 ↔ ∃𝑦 ∈ 𝑥 𝜑) → ∃𝑡∀𝑧(𝑧 ∈ 𝑡 ↔ ∃𝑦 ∈ 𝑥 𝜑))
55	53, 54	syl6 35	. 2 ⊢ (∀𝑦 ∈ 𝑥 ∃*𝑧𝜑 → (∃𝑠∀𝑦(𝑦 ∈ 𝑠 ↔ (𝑦 ∈ 𝑥 ∧ ∃𝑧𝜑)) → ∃𝑡∀𝑧(𝑧 ∈ 𝑡 ↔ ∃𝑦 ∈ 𝑥 𝜑)))
56		bj-axreprepsep.axsep	. 2 ⊢ ∀𝑥∃𝑠∀𝑦(𝑦 ∈ 𝑠 ↔ (𝑦 ∈ 𝑥 ∧ ∃𝑧𝜑))
57	55, 56	bj-almpig 36835	1 ⊢ ∀𝑥(∀𝑦 ∈ 𝑥 ∃*𝑧𝜑 → ∃𝑡∀𝑧(𝑧 ∈ 𝑡 ↔ ∃𝑦 ∈ 𝑥 𝜑))

Syntax hints:   → wi 4   ↔ wb 206   ∧ wa 395  ∀wal 1540  ∃wex 1781  ∃*wmo 2538  ∃!weu 2569  ∀wral 3052  ∃wrex 3062

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-10 2147  ax-11 2163  ax-12 2185

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-tru 1545  df-ex 1782  df-nf 1786  df-eu 2570  df-ral 3053  df-rex 3063

This theorem is referenced by: (None)