Theorem bj-axseprep 37655

Description: Axiom of separation (universal closure of ax-sep 5256) from a weak form of the axiom of replacement requiring that the functional relation in it be a (total) function and the weak emptyset axiom (existence of an empty set provided existence of a set), as written in the theorem's hypotheses.

This result shows that the weak emptyset axiom is not only the result of a cheap way to avoid an axiom redundancy (in this case, the existence axiom extru 2003) by adding it as an antecedent, but also permits to prove nontrivial results that hold in nonnecessarily nonempty universes.

This proof is by cases so is not intuitionistic. The statement does not require a nonempty universe; most of the proof does not either, and the parts that do (e.g., near sb8ef 2385 and sbequ12r 2286 and eueq2 3672) could be reworked to avoid it. Proof modifications should not introduce steps relying on a nonempty universe, like alrimiv 1955. (Contributed by BJ, 14-Mar-2026.) (Proof modification is discouraged.)

Hypotheses

Ref	Expression
bj-axseprep.axnulw	⊢ (∃𝑥⊤ → ∃𝑦∀𝑧 ∈ 𝑦 ⊥)
bj-axseprep.axrep	⊢ ∀𝑥(∀𝑧 ∈ 𝑥 ∃!𝑡𝜓 → ∃𝑦∀𝑡(𝑡 ∈ 𝑦 ↔ ∃𝑧 ∈ 𝑥 𝜓))
bj-axseprep.ps	⊢ (𝜓 ↔ ((𝜑 ∧ 𝑡 = 𝑧) ∨ (¬ 𝜑 ∧ 𝑡 = 𝑎)))

Assertion

Ref	Expression
bj-axseprep	⊢ ∀𝑥∃𝑦∀𝑧(𝑧 ∈ 𝑦 ↔ (𝑧 ∈ 𝑥 ∧ 𝜑))

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

Allowed substitution hints:   𝜑(𝑧)   𝜓(𝑥,𝑦,𝑧,𝑡,𝑎)

Proof of Theorem bj-axseprep

Step	Hyp	Ref	Expression
1		ax5e 1940	. . . 4 ⊢ (∃𝑎∃𝑦∀𝑧(𝑧 ∈ 𝑦 ↔ (𝑧 ∈ 𝑥 ∧ 𝜑)) → ∃𝑦∀𝑧(𝑧 ∈ 𝑦 ↔ (𝑧 ∈ 𝑥 ∧ 𝜑)))
2	1	ax-gen 1823	. . 3 ⊢ ∀𝑥(∃𝑎∃𝑦∀𝑧(𝑧 ∈ 𝑦 ↔ (𝑧 ∈ 𝑥 ∧ 𝜑)) → ∃𝑦∀𝑧(𝑧 ∈ 𝑦 ↔ (𝑧 ∈ 𝑥 ∧ 𝜑)))
3		bj-eximcom 37183	. . . . 5 ⊢ (∃𝑎(∃𝑦∀𝑡(𝑡 ∈ 𝑦 ↔ ∃𝑧 ∈ 𝑥 ((𝜑 ∧ 𝑡 = 𝑧) ∨ (¬ 𝜑 ∧ 𝑡 = 𝑎))) → ∃𝑦∀𝑧(𝑧 ∈ 𝑦 ↔ (𝑧 ∈ 𝑥 ∧ 𝜑))) → (∀𝑎∃𝑦∀𝑡(𝑡 ∈ 𝑦 ↔ ∃𝑧 ∈ 𝑥 ((𝜑 ∧ 𝑡 = 𝑧) ∨ (¬ 𝜑 ∧ 𝑡 = 𝑎))) → ∃𝑎∃𝑦∀𝑧(𝑧 ∈ 𝑦 ↔ (𝑧 ∈ 𝑥 ∧ 𝜑))))
4		bj-axseprep.axrep	. . . . . . . . 9 ⊢ ∀𝑥(∀𝑧 ∈ 𝑥 ∃!𝑡𝜓 → ∃𝑦∀𝑡(𝑡 ∈ 𝑦 ↔ ∃𝑧 ∈ 𝑥 𝜓))
5		bj-axseprep.ps	. . . . . . . . . . . . 13 ⊢ (𝜓 ↔ ((𝜑 ∧ 𝑡 = 𝑧) ∨ (¬ 𝜑 ∧ 𝑡 = 𝑎)))
6	5	eubii 2611	. . . . . . . . . . . 12 ⊢ (∃!𝑡𝜓 ↔ ∃!𝑡((𝜑 ∧ 𝑡 = 𝑧) ∨ (¬ 𝜑 ∧ 𝑡 = 𝑎)))
7	6	ralbii 3109	. . . . . . . . . . 11 ⊢ (∀𝑧 ∈ 𝑥 ∃!𝑡𝜓 ↔ ∀𝑧 ∈ 𝑥 ∃!𝑡((𝜑 ∧ 𝑡 = 𝑧) ∨ (¬ 𝜑 ∧ 𝑡 = 𝑎)))
8	5	rexbii 3110	. . . . . . . . . . . . . 14 ⊢ (∃𝑧 ∈ 𝑥 𝜓 ↔ ∃𝑧 ∈ 𝑥 ((𝜑 ∧ 𝑡 = 𝑧) ∨ (¬ 𝜑 ∧ 𝑡 = 𝑎)))
9	8	bibi2i 340	. . . . . . . . . . . . 13 ⊢ ((𝑡 ∈ 𝑦 ↔ ∃𝑧 ∈ 𝑥 𝜓) ↔ (𝑡 ∈ 𝑦 ↔ ∃𝑧 ∈ 𝑥 ((𝜑 ∧ 𝑡 = 𝑧) ∨ (¬ 𝜑 ∧ 𝑡 = 𝑎))))
10	9	albii 1847	. . . . . . . . . . . 12 ⊢ (∀𝑡(𝑡 ∈ 𝑦 ↔ ∃𝑧 ∈ 𝑥 𝜓) ↔ ∀𝑡(𝑡 ∈ 𝑦 ↔ ∃𝑧 ∈ 𝑥 ((𝜑 ∧ 𝑡 = 𝑧) ∨ (¬ 𝜑 ∧ 𝑡 = 𝑎))))
11	10	exbii 1876	. . . . . . . . . . 11 ⊢ (∃𝑦∀𝑡(𝑡 ∈ 𝑦 ↔ ∃𝑧 ∈ 𝑥 𝜓) ↔ ∃𝑦∀𝑡(𝑡 ∈ 𝑦 ↔ ∃𝑧 ∈ 𝑥 ((𝜑 ∧ 𝑡 = 𝑧) ∨ (¬ 𝜑 ∧ 𝑡 = 𝑎))))
12	7, 11	imbi12i 353	. . . . . . . . . 10 ⊢ ((∀𝑧 ∈ 𝑥 ∃!𝑡𝜓 → ∃𝑦∀𝑡(𝑡 ∈ 𝑦 ↔ ∃𝑧 ∈ 𝑥 𝜓)) ↔ (∀𝑧 ∈ 𝑥 ∃!𝑡((𝜑 ∧ 𝑡 = 𝑧) ∨ (¬ 𝜑 ∧ 𝑡 = 𝑎)) → ∃𝑦∀𝑡(𝑡 ∈ 𝑦 ↔ ∃𝑧 ∈ 𝑥 ((𝜑 ∧ 𝑡 = 𝑧) ∨ (¬ 𝜑 ∧ 𝑡 = 𝑎)))))
13	12	albii 1847	. . . . . . . . 9 ⊢ (∀𝑥(∀𝑧 ∈ 𝑥 ∃!𝑡𝜓 → ∃𝑦∀𝑡(𝑡 ∈ 𝑦 ↔ ∃𝑧 ∈ 𝑥 𝜓)) ↔ ∀𝑥(∀𝑧 ∈ 𝑥 ∃!𝑡((𝜑 ∧ 𝑡 = 𝑧) ∨ (¬ 𝜑 ∧ 𝑡 = 𝑎)) → ∃𝑦∀𝑡(𝑡 ∈ 𝑦 ↔ ∃𝑧 ∈ 𝑥 ((𝜑 ∧ 𝑡 = 𝑧) ∨ (¬ 𝜑 ∧ 𝑡 = 𝑎)))))
14	4, 13	mpbi 233	. . . . . . . 8 ⊢ ∀𝑥(∀𝑧 ∈ 𝑥 ∃!𝑡((𝜑 ∧ 𝑡 = 𝑧) ∨ (¬ 𝜑 ∧ 𝑡 = 𝑎)) → ∃𝑦∀𝑡(𝑡 ∈ 𝑦 ↔ ∃𝑧 ∈ 𝑥 ((𝜑 ∧ 𝑡 = 𝑧) ∨ (¬ 𝜑 ∧ 𝑡 = 𝑎))))
15		vex 3457	. . . . . . . . . . 11 ⊢ 𝑧 ∈ V
16		vex 3457	. . . . . . . . . . 11 ⊢ 𝑎 ∈ V
17	15, 16	eueq2 3672	. . . . . . . . . 10 ⊢ ∃!𝑡((𝜑 ∧ 𝑡 = 𝑧) ∨ (¬ 𝜑 ∧ 𝑡 = 𝑎))
18	17	rgenw 3081	. . . . . . . . 9 ⊢ ∀𝑧 ∈ 𝑥 ∃!𝑡((𝜑 ∧ 𝑡 = 𝑧) ∨ (¬ 𝜑 ∧ 𝑡 = 𝑎))
19	18	ax-gen 1823	. . . . . . . 8 ⊢ ∀𝑥∀𝑧 ∈ 𝑥 ∃!𝑡((𝜑 ∧ 𝑡 = 𝑧) ∨ (¬ 𝜑 ∧ 𝑡 = 𝑎))
20	14, 19	bj-almp 37148	. . . . . . 7 ⊢ ∀𝑥∃𝑦∀𝑡(𝑡 ∈ 𝑦 ↔ ∃𝑧 ∈ 𝑥 ((𝜑 ∧ 𝑡 = 𝑧) ∨ (¬ 𝜑 ∧ 𝑡 = 𝑎)))
21	20	ax-gen 1823	. . . . . 6 ⊢ ∀𝑎∀𝑥∃𝑦∀𝑡(𝑡 ∈ 𝑦 ↔ ∃𝑧 ∈ 𝑥 ((𝜑 ∧ 𝑡 = 𝑧) ∨ (¬ 𝜑 ∧ 𝑡 = 𝑎)))
22		alcom 2192	. . . . . 6 ⊢ (∀𝑎∀𝑥∃𝑦∀𝑡(𝑡 ∈ 𝑦 ↔ ∃𝑧 ∈ 𝑥 ((𝜑 ∧ 𝑡 = 𝑧) ∨ (¬ 𝜑 ∧ 𝑡 = 𝑎))) ↔ ∀𝑥∀𝑎∃𝑦∀𝑡(𝑡 ∈ 𝑦 ↔ ∃𝑧 ∈ 𝑥 ((𝜑 ∧ 𝑡 = 𝑧) ∨ (¬ 𝜑 ∧ 𝑡 = 𝑎))))
23	21, 22	mpbi 233	. . . . 5 ⊢ ∀𝑥∀𝑎∃𝑦∀𝑡(𝑡 ∈ 𝑦 ↔ ∃𝑧 ∈ 𝑥 ((𝜑 ∧ 𝑡 = 𝑧) ∨ (¬ 𝜑 ∧ 𝑡 = 𝑎)))
24	3, 23	bj-almpig 37157	. . . 4 ⊢ ∀𝑥(∃𝑎(∃𝑦∀𝑡(𝑡 ∈ 𝑦 ↔ ∃𝑧 ∈ 𝑥 ((𝜑 ∧ 𝑡 = 𝑧) ∨ (¬ 𝜑 ∧ 𝑡 = 𝑎))) → ∃𝑦∀𝑧(𝑧 ∈ 𝑦 ↔ (𝑧 ∈ 𝑥 ∧ 𝜑))) → ∃𝑎∃𝑦∀𝑧(𝑧 ∈ 𝑦 ↔ (𝑧 ∈ 𝑥 ∧ 𝜑)))
25		df-rex 3088	. . . . . . 7 ⊢ (∃𝑧 ∈ 𝑥 𝜑 ↔ ∃𝑧(𝑧 ∈ 𝑥 ∧ 𝜑))
26		nfv 1942	. . . . . . . 8 ⊢ Ⅎ𝑎(𝑧 ∈ 𝑥 ∧ 𝜑)
27	26	sb8ef 2385	. . . . . . 7 ⊢ (∃𝑧(𝑧 ∈ 𝑥 ∧ 𝜑) ↔ ∃𝑎[𝑎 / 𝑧](𝑧 ∈ 𝑥 ∧ 𝜑))
28	25, 27	bitri 278	. . . . . 6 ⊢ (∃𝑧 ∈ 𝑥 𝜑 ↔ ∃𝑎[𝑎 / 𝑧](𝑧 ∈ 𝑥 ∧ 𝜑))
29		df-rex 3088	. . . . . . . . . . . . . 14 ⊢ (∃𝑧 ∈ 𝑥 ((𝜑 ∧ 𝑡 = 𝑧) ∨ (¬ 𝜑 ∧ 𝑡 = 𝑎)) ↔ ∃𝑧(𝑧 ∈ 𝑥 ∧ ((𝜑 ∧ 𝑡 = 𝑧) ∨ (¬ 𝜑 ∧ 𝑡 = 𝑎))))
30		andi 1023	. . . . . . . . . . . . . . 15 ⊢ ((𝑧 ∈ 𝑥 ∧ ((𝜑 ∧ 𝑡 = 𝑧) ∨ (¬ 𝜑 ∧ 𝑡 = 𝑎))) ↔ ((𝑧 ∈ 𝑥 ∧ (𝜑 ∧ 𝑡 = 𝑧)) ∨ (𝑧 ∈ 𝑥 ∧ (¬ 𝜑 ∧ 𝑡 = 𝑎))))
31	30	exbii 1876	. . . . . . . . . . . . . 14 ⊢ (∃𝑧(𝑧 ∈ 𝑥 ∧ ((𝜑 ∧ 𝑡 = 𝑧) ∨ (¬ 𝜑 ∧ 𝑡 = 𝑎))) ↔ ∃𝑧((𝑧 ∈ 𝑥 ∧ (𝜑 ∧ 𝑡 = 𝑧)) ∨ (𝑧 ∈ 𝑥 ∧ (¬ 𝜑 ∧ 𝑡 = 𝑎))))
32		19.43 1910	. . . . . . . . . . . . . 14 ⊢ (∃𝑧((𝑧 ∈ 𝑥 ∧ (𝜑 ∧ 𝑡 = 𝑧)) ∨ (𝑧 ∈ 𝑥 ∧ (¬ 𝜑 ∧ 𝑡 = 𝑎))) ↔ (∃𝑧(𝑧 ∈ 𝑥 ∧ (𝜑 ∧ 𝑡 = 𝑧)) ∨ ∃𝑧(𝑧 ∈ 𝑥 ∧ (¬ 𝜑 ∧ 𝑡 = 𝑎))))
33	29, 31, 32	3bitri 300	. . . . . . . . . . . . 13 ⊢ (∃𝑧 ∈ 𝑥 ((𝜑 ∧ 𝑡 = 𝑧) ∨ (¬ 𝜑 ∧ 𝑡 = 𝑎)) ↔ (∃𝑧(𝑧 ∈ 𝑥 ∧ (𝜑 ∧ 𝑡 = 𝑧)) ∨ ∃𝑧(𝑧 ∈ 𝑥 ∧ (¬ 𝜑 ∧ 𝑡 = 𝑎))))
34		equcom 2046	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑧 = 𝑡 ↔ 𝑡 = 𝑧)
35	34	anbi1i 635	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑧 = 𝑡 ∧ (𝑧 ∈ 𝑥 ∧ 𝜑)) ↔ (𝑡 = 𝑧 ∧ (𝑧 ∈ 𝑥 ∧ 𝜑)))
36		ancom 465	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑡 = 𝑧 ∧ (𝑧 ∈ 𝑥 ∧ 𝜑)) ↔ ((𝑧 ∈ 𝑥 ∧ 𝜑) ∧ 𝑡 = 𝑧))
37		anass 473	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝑧 ∈ 𝑥 ∧ 𝜑) ∧ 𝑡 = 𝑧) ↔ (𝑧 ∈ 𝑥 ∧ (𝜑 ∧ 𝑡 = 𝑧)))
38	35, 36, 37	3bitri 300	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑧 = 𝑡 ∧ (𝑧 ∈ 𝑥 ∧ 𝜑)) ↔ (𝑧 ∈ 𝑥 ∧ (𝜑 ∧ 𝑡 = 𝑧)))
39	38	exbii 1876	. . . . . . . . . . . . . . . . 17 ⊢ (∃𝑧(𝑧 = 𝑡 ∧ (𝑧 ∈ 𝑥 ∧ 𝜑)) ↔ ∃𝑧(𝑧 ∈ 𝑥 ∧ (𝜑 ∧ 𝑡 = 𝑧)))
40	39	biimpri 231	. . . . . . . . . . . . . . . 16 ⊢ (∃𝑧(𝑧 ∈ 𝑥 ∧ (𝜑 ∧ 𝑡 = 𝑧)) → ∃𝑧(𝑧 = 𝑡 ∧ (𝑧 ∈ 𝑥 ∧ 𝜑)))
41	40	a1i 11	. . . . . . . . . . . . . . 15 ⊢ ([𝑎 / 𝑧](𝑧 ∈ 𝑥 ∧ 𝜑) → (∃𝑧(𝑧 ∈ 𝑥 ∧ (𝜑 ∧ 𝑡 = 𝑧)) → ∃𝑧(𝑧 = 𝑡 ∧ (𝑧 ∈ 𝑥 ∧ 𝜑))))
42		simprr 784	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑧 ∈ 𝑥 ∧ (¬ 𝜑 ∧ 𝑡 = 𝑎)) → 𝑡 = 𝑎)
43	42	exlimiv 1958	. . . . . . . . . . . . . . . 16 ⊢ (∃𝑧(𝑧 ∈ 𝑥 ∧ (¬ 𝜑 ∧ 𝑡 = 𝑎)) → 𝑡 = 𝑎)
44		sbequi 2116	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑎 = 𝑡 → ([𝑎 / 𝑧](𝑧 ∈ 𝑥 ∧ 𝜑) → [𝑡 / 𝑧](𝑧 ∈ 𝑥 ∧ 𝜑)))
45	44	equcoms 2048	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑡 = 𝑎 → ([𝑎 / 𝑧](𝑧 ∈ 𝑥 ∧ 𝜑) → [𝑡 / 𝑧](𝑧 ∈ 𝑥 ∧ 𝜑)))
46	45	com12 33	. . . . . . . . . . . . . . . . 17 ⊢ ([𝑎 / 𝑧](𝑧 ∈ 𝑥 ∧ 𝜑) → (𝑡 = 𝑎 → [𝑡 / 𝑧](𝑧 ∈ 𝑥 ∧ 𝜑)))
47		sb5 2309	. . . . . . . . . . . . . . . . 17 ⊢ ([𝑡 / 𝑧](𝑧 ∈ 𝑥 ∧ 𝜑) ↔ ∃𝑧(𝑧 = 𝑡 ∧ (𝑧 ∈ 𝑥 ∧ 𝜑)))
48	46, 47	imbitrdi 254	. . . . . . . . . . . . . . . 16 ⊢ ([𝑎 / 𝑧](𝑧 ∈ 𝑥 ∧ 𝜑) → (𝑡 = 𝑎 → ∃𝑧(𝑧 = 𝑡 ∧ (𝑧 ∈ 𝑥 ∧ 𝜑))))
49	43, 48	syl5 35	. . . . . . . . . . . . . . 15 ⊢ ([𝑎 / 𝑧](𝑧 ∈ 𝑥 ∧ 𝜑) → (∃𝑧(𝑧 ∈ 𝑥 ∧ (¬ 𝜑 ∧ 𝑡 = 𝑎)) → ∃𝑧(𝑧 = 𝑡 ∧ (𝑧 ∈ 𝑥 ∧ 𝜑))))
50	41, 49	jaod 872	. . . . . . . . . . . . . 14 ⊢ ([𝑎 / 𝑧](𝑧 ∈ 𝑥 ∧ 𝜑) → ((∃𝑧(𝑧 ∈ 𝑥 ∧ (𝜑 ∧ 𝑡 = 𝑧)) ∨ ∃𝑧(𝑧 ∈ 𝑥 ∧ (¬ 𝜑 ∧ 𝑡 = 𝑎))) → ∃𝑧(𝑧 = 𝑡 ∧ (𝑧 ∈ 𝑥 ∧ 𝜑))))
51		orc 880	. . . . . . . . . . . . . . 15 ⊢ (∃𝑧(𝑧 ∈ 𝑥 ∧ (𝜑 ∧ 𝑡 = 𝑧)) → (∃𝑧(𝑧 ∈ 𝑥 ∧ (𝜑 ∧ 𝑡 = 𝑧)) ∨ ∃𝑧(𝑧 ∈ 𝑥 ∧ (¬ 𝜑 ∧ 𝑡 = 𝑎))))
52	39, 51	sylbi 220	. . . . . . . . . . . . . 14 ⊢ (∃𝑧(𝑧 = 𝑡 ∧ (𝑧 ∈ 𝑥 ∧ 𝜑)) → (∃𝑧(𝑧 ∈ 𝑥 ∧ (𝜑 ∧ 𝑡 = 𝑧)) ∨ ∃𝑧(𝑧 ∈ 𝑥 ∧ (¬ 𝜑 ∧ 𝑡 = 𝑎))))
53	50, 52	impbid1 228	. . . . . . . . . . . . 13 ⊢ ([𝑎 / 𝑧](𝑧 ∈ 𝑥 ∧ 𝜑) → ((∃𝑧(𝑧 ∈ 𝑥 ∧ (𝜑 ∧ 𝑡 = 𝑧)) ∨ ∃𝑧(𝑧 ∈ 𝑥 ∧ (¬ 𝜑 ∧ 𝑡 = 𝑎))) ↔ ∃𝑧(𝑧 = 𝑡 ∧ (𝑧 ∈ 𝑥 ∧ 𝜑))))
54	33, 53	bitrid 286	. . . . . . . . . . . 12 ⊢ ([𝑎 / 𝑧](𝑧 ∈ 𝑥 ∧ 𝜑) → (∃𝑧 ∈ 𝑥 ((𝜑 ∧ 𝑡 = 𝑧) ∨ (¬ 𝜑 ∧ 𝑡 = 𝑎)) ↔ ∃𝑧(𝑧 = 𝑡 ∧ (𝑧 ∈ 𝑥 ∧ 𝜑))))
55	54	bibi2d 345	. . . . . . . . . . 11 ⊢ ([𝑎 / 𝑧](𝑧 ∈ 𝑥 ∧ 𝜑) → ((𝑡 ∈ 𝑦 ↔ ∃𝑧 ∈ 𝑥 ((𝜑 ∧ 𝑡 = 𝑧) ∨ (¬ 𝜑 ∧ 𝑡 = 𝑎))) ↔ (𝑡 ∈ 𝑦 ↔ ∃𝑧(𝑧 = 𝑡 ∧ (𝑧 ∈ 𝑥 ∧ 𝜑)))))
56	55	biimpd 232	. . . . . . . . . 10 ⊢ ([𝑎 / 𝑧](𝑧 ∈ 𝑥 ∧ 𝜑) → ((𝑡 ∈ 𝑦 ↔ ∃𝑧 ∈ 𝑥 ((𝜑 ∧ 𝑡 = 𝑧) ∨ (¬ 𝜑 ∧ 𝑡 = 𝑎))) → (𝑡 ∈ 𝑦 ↔ ∃𝑧(𝑧 = 𝑡 ∧ (𝑧 ∈ 𝑥 ∧ 𝜑)))))
57	56	alimdv 1944	. . . . . . . . 9 ⊢ ([𝑎 / 𝑧](𝑧 ∈ 𝑥 ∧ 𝜑) → (∀𝑡(𝑡 ∈ 𝑦 ↔ ∃𝑧 ∈ 𝑥 ((𝜑 ∧ 𝑡 = 𝑧) ∨ (¬ 𝜑 ∧ 𝑡 = 𝑎))) → ∀𝑡(𝑡 ∈ 𝑦 ↔ ∃𝑧(𝑧 = 𝑡 ∧ (𝑧 ∈ 𝑥 ∧ 𝜑)))))
58		nfv 1942	. . . . . . . . . . 11 ⊢ Ⅎ𝑧 𝑡 ∈ 𝑦
59		nfe1 2183	. . . . . . . . . . 11 ⊢ Ⅎ𝑧∃𝑧(𝑧 = 𝑡 ∧ (𝑧 ∈ 𝑥 ∧ 𝜑))
60	58, 59	nfbi 1931	. . . . . . . . . 10 ⊢ Ⅎ𝑧(𝑡 ∈ 𝑦 ↔ ∃𝑧(𝑧 = 𝑡 ∧ (𝑧 ∈ 𝑥 ∧ 𝜑)))
61		nfv 1942	. . . . . . . . . 10 ⊢ Ⅎ𝑡(𝑧 ∈ 𝑦 ↔ (𝑧 ∈ 𝑥 ∧ 𝜑))
62		elequ1 2148	. . . . . . . . . . 11 ⊢ (𝑡 = 𝑧 → (𝑡 ∈ 𝑦 ↔ 𝑧 ∈ 𝑦))
63	47	bicomi 227	. . . . . . . . . . . 12 ⊢ (∃𝑧(𝑧 = 𝑡 ∧ (𝑧 ∈ 𝑥 ∧ 𝜑)) ↔ [𝑡 / 𝑧](𝑧 ∈ 𝑥 ∧ 𝜑))
64		sbequ12r 2286	. . . . . . . . . . . 12 ⊢ (𝑡 = 𝑧 → ([𝑡 / 𝑧](𝑧 ∈ 𝑥 ∧ 𝜑) ↔ (𝑧 ∈ 𝑥 ∧ 𝜑)))
65	63, 64	bitrid 286	. . . . . . . . . . 11 ⊢ (𝑡 = 𝑧 → (∃𝑧(𝑧 = 𝑡 ∧ (𝑧 ∈ 𝑥 ∧ 𝜑)) ↔ (𝑧 ∈ 𝑥 ∧ 𝜑)))
66	62, 65	bibi12d 348	. . . . . . . . . 10 ⊢ (𝑡 = 𝑧 → ((𝑡 ∈ 𝑦 ↔ ∃𝑧(𝑧 = 𝑡 ∧ (𝑧 ∈ 𝑥 ∧ 𝜑))) ↔ (𝑧 ∈ 𝑦 ↔ (𝑧 ∈ 𝑥 ∧ 𝜑))))
67	60, 61, 66	cbvalv1 2371	. . . . . . . . 9 ⊢ (∀𝑡(𝑡 ∈ 𝑦 ↔ ∃𝑧(𝑧 = 𝑡 ∧ (𝑧 ∈ 𝑥 ∧ 𝜑))) ↔ ∀𝑧(𝑧 ∈ 𝑦 ↔ (𝑧 ∈ 𝑥 ∧ 𝜑)))
68	57, 67	imbitrdi 254	. . . . . . . 8 ⊢ ([𝑎 / 𝑧](𝑧 ∈ 𝑥 ∧ 𝜑) → (∀𝑡(𝑡 ∈ 𝑦 ↔ ∃𝑧 ∈ 𝑥 ((𝜑 ∧ 𝑡 = 𝑧) ∨ (¬ 𝜑 ∧ 𝑡 = 𝑎))) → ∀𝑧(𝑧 ∈ 𝑦 ↔ (𝑧 ∈ 𝑥 ∧ 𝜑))))
69	68	eximdv 1945	. . . . . . 7 ⊢ ([𝑎 / 𝑧](𝑧 ∈ 𝑥 ∧ 𝜑) → (∃𝑦∀𝑡(𝑡 ∈ 𝑦 ↔ ∃𝑧 ∈ 𝑥 ((𝜑 ∧ 𝑡 = 𝑧) ∨ (¬ 𝜑 ∧ 𝑡 = 𝑎))) → ∃𝑦∀𝑧(𝑧 ∈ 𝑦 ↔ (𝑧 ∈ 𝑥 ∧ 𝜑))))
70	69	eximi 1863	. . . . . 6 ⊢ (∃𝑎[𝑎 / 𝑧](𝑧 ∈ 𝑥 ∧ 𝜑) → ∃𝑎(∃𝑦∀𝑡(𝑡 ∈ 𝑦 ↔ ∃𝑧 ∈ 𝑥 ((𝜑 ∧ 𝑡 = 𝑧) ∨ (¬ 𝜑 ∧ 𝑡 = 𝑎))) → ∃𝑦∀𝑧(𝑧 ∈ 𝑦 ↔ (𝑧 ∈ 𝑥 ∧ 𝜑))))
71	28, 70	sylbi 220	. . . . 5 ⊢ (∃𝑧 ∈ 𝑥 𝜑 → ∃𝑎(∃𝑦∀𝑡(𝑡 ∈ 𝑦 ↔ ∃𝑧 ∈ 𝑥 ((𝜑 ∧ 𝑡 = 𝑧) ∨ (¬ 𝜑 ∧ 𝑡 = 𝑎))) → ∃𝑦∀𝑧(𝑧 ∈ 𝑦 ↔ (𝑧 ∈ 𝑥 ∧ 𝜑))))
72	71	ax-gen 1823	. . . 4 ⊢ ∀𝑥(∃𝑧 ∈ 𝑥 𝜑 → ∃𝑎(∃𝑦∀𝑡(𝑡 ∈ 𝑦 ↔ ∃𝑧 ∈ 𝑥 ((𝜑 ∧ 𝑡 = 𝑧) ∨ (¬ 𝜑 ∧ 𝑡 = 𝑎))) → ∃𝑦∀𝑧(𝑧 ∈ 𝑦 ↔ (𝑧 ∈ 𝑥 ∧ 𝜑))))
73	24, 72	barbara 2688	. . 3 ⊢ ∀𝑥(∃𝑧 ∈ 𝑥 𝜑 → ∃𝑎∃𝑦∀𝑧(𝑧 ∈ 𝑦 ↔ (𝑧 ∈ 𝑥 ∧ 𝜑)))
74	2, 73	barbara 2688	. 2 ⊢ ∀𝑥(∃𝑧 ∈ 𝑥 𝜑 → ∃𝑦∀𝑧(𝑧 ∈ 𝑦 ↔ (𝑧 ∈ 𝑥 ∧ 𝜑)))
75		ralnex 3089	. . . . 5 ⊢ (∀𝑧 ∈ 𝑥 ¬ 𝜑 ↔ ¬ ∃𝑧 ∈ 𝑥 𝜑)
76		df-ral 3078	. . . . . 6 ⊢ (∀𝑧 ∈ 𝑥 ¬ 𝜑 ↔ ∀𝑧(𝑧 ∈ 𝑥 → ¬ 𝜑))
77		df-ral 3078	. . . . . . 7 ⊢ (∀𝑧 ∈ 𝑦 ⊥ ↔ ∀𝑧(𝑧 ∈ 𝑦 → ⊥))
78		dfnot 1587	. . . . . . . . . . 11 ⊢ (¬ 𝑧 ∈ 𝑦 ↔ (𝑧 ∈ 𝑦 → ⊥))
79	78	bicomi 227	. . . . . . . . . 10 ⊢ ((𝑧 ∈ 𝑦 → ⊥) ↔ ¬ 𝑧 ∈ 𝑦)
80		imnan 404	. . . . . . . . . 10 ⊢ ((𝑧 ∈ 𝑥 → ¬ 𝜑) ↔ ¬ (𝑧 ∈ 𝑥 ∧ 𝜑))
81		pm5.21 836	. . . . . . . . . 10 ⊢ ((¬ 𝑧 ∈ 𝑦 ∧ ¬ (𝑧 ∈ 𝑥 ∧ 𝜑)) → (𝑧 ∈ 𝑦 ↔ (𝑧 ∈ 𝑥 ∧ 𝜑)))
82	79, 80, 81	syl2anb 609	. . . . . . . . 9 ⊢ (((𝑧 ∈ 𝑦 → ⊥) ∧ (𝑧 ∈ 𝑥 → ¬ 𝜑)) → (𝑧 ∈ 𝑦 ↔ (𝑧 ∈ 𝑥 ∧ 𝜑)))
83	82	expcom 418	. . . . . . . 8 ⊢ ((𝑧 ∈ 𝑥 → ¬ 𝜑) → ((𝑧 ∈ 𝑦 → ⊥) → (𝑧 ∈ 𝑦 ↔ (𝑧 ∈ 𝑥 ∧ 𝜑))))
84	83	al2imi 1843	. . . . . . 7 ⊢ (∀𝑧(𝑧 ∈ 𝑥 → ¬ 𝜑) → (∀𝑧(𝑧 ∈ 𝑦 → ⊥) → ∀𝑧(𝑧 ∈ 𝑦 ↔ (𝑧 ∈ 𝑥 ∧ 𝜑))))
85	77, 84	biimtrid 245	. . . . . 6 ⊢ (∀𝑧(𝑧 ∈ 𝑥 → ¬ 𝜑) → (∀𝑧 ∈ 𝑦 ⊥ → ∀𝑧(𝑧 ∈ 𝑦 ↔ (𝑧 ∈ 𝑥 ∧ 𝜑))))
86	76, 85	sylbi 220	. . . . 5 ⊢ (∀𝑧 ∈ 𝑥 ¬ 𝜑 → (∀𝑧 ∈ 𝑦 ⊥ → ∀𝑧(𝑧 ∈ 𝑦 ↔ (𝑧 ∈ 𝑥 ∧ 𝜑))))
87	75, 86	sylbir 238	. . . 4 ⊢ (¬ ∃𝑧 ∈ 𝑥 𝜑 → (∀𝑧 ∈ 𝑦 ⊥ → ∀𝑧(𝑧 ∈ 𝑦 ↔ (𝑧 ∈ 𝑥 ∧ 𝜑))))
88	87	eximdv 1945	. . 3 ⊢ (¬ ∃𝑧 ∈ 𝑥 𝜑 → (∃𝑦∀𝑧 ∈ 𝑦 ⊥ → ∃𝑦∀𝑧(𝑧 ∈ 𝑦 ↔ (𝑧 ∈ 𝑥 ∧ 𝜑))))
89		bj-axseprep.axnulw	. . . 4 ⊢ (∃𝑥⊤ → ∃𝑦∀𝑧 ∈ 𝑦 ⊥)
90		bj-alextruim 37203	. . . 4 ⊢ (∀𝑥∃𝑦∀𝑧 ∈ 𝑦 ⊥ ↔ (∃𝑥⊤ → ∃𝑦∀𝑧 ∈ 𝑦 ⊥))
91	89, 90	mpbir 234	. . 3 ⊢ ∀𝑥∃𝑦∀𝑧 ∈ 𝑦 ⊥
92	88, 91	bj-almpig 37157	. 2 ⊢ ∀𝑥(¬ ∃𝑧 ∈ 𝑥 𝜑 → ∃𝑦∀𝑧(𝑧 ∈ 𝑦 ↔ (𝑧 ∈ 𝑥 ∧ 𝜑)))
93		pm2.61 194	. . 3 ⊢ ((∃𝑧 ∈ 𝑥 𝜑 → ∃𝑦∀𝑧(𝑧 ∈ 𝑦 ↔ (𝑧 ∈ 𝑥 ∧ 𝜑))) → ((¬ ∃𝑧 ∈ 𝑥 𝜑 → ∃𝑦∀𝑧(𝑧 ∈ 𝑦 ↔ (𝑧 ∈ 𝑥 ∧ 𝜑))) → ∃𝑦∀𝑧(𝑧 ∈ 𝑦 ↔ (𝑧 ∈ 𝑥 ∧ 𝜑))))
94	93	al2imi 1843	. 2 ⊢ (∀𝑥(∃𝑧 ∈ 𝑥 𝜑 → ∃𝑦∀𝑧(𝑧 ∈ 𝑦 ↔ (𝑧 ∈ 𝑥 ∧ 𝜑))) → (∀𝑥(¬ ∃𝑧 ∈ 𝑥 𝜑 → ∃𝑦∀𝑧(𝑧 ∈ 𝑦 ↔ (𝑧 ∈ 𝑥 ∧ 𝜑))) → ∀𝑥∃𝑦∀𝑧(𝑧 ∈ 𝑦 ↔ (𝑧 ∈ 𝑥 ∧ 𝜑))))
95	74, 92, 94	mp2 9	1 ⊢ ∀𝑥∃𝑦∀𝑧(𝑧 ∈ 𝑦 ↔ (𝑧 ∈ 𝑥 ∧ 𝜑))

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 209   ∧ wa 400   ∨ wo 860  ∀wal 1566   = wceq 1568  ⊤wtru 1569  ⊥wfal 1580  ∃wex 1807  [wsb 2094   ∈ wcel 2141  ∃!weu 2594  ∀wral 3077  ∃wrex 3087

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1823  ax-4 1837  ax-5 1938  ax-6 1995  ax-7 2036  ax-8 2143  ax-9 2151  ax-10 2174  ax-11 2190  ax-12 2211  ax-ext 2733

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-tru 1571  df-fal 1581  df-ex 1808  df-nf 1812  df-sb 2095  df-mo 2565  df-eu 2595  df-clab 2740  df-cleq 2753  df-clel 2836  df-ral 3078  df-rex 3088  df-v 3455

This theorem is referenced by: (None)