Theorem bj-axseprep 37910

Description: Axiom of separation (universal closure of ax-sep 5248) 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 2008) 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 2384 and sbequ12r 2287 and eueq2 3667) could be reworked to avoid it. Proof modifications should not introduce steps relying on a nonempty universe, like alrimiv 1960. (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 1945	. . . 4 ⊢ (∃𝑎∃𝑦∀𝑧(𝑧 ∈ 𝑦 ↔ (𝑧 ∈ 𝑥 ∧ 𝜑)) → ∃𝑦∀𝑧(𝑧 ∈ 𝑦 ↔ (𝑧 ∈ 𝑥 ∧ 𝜑)))
2	1	ax-gen 1828	. . 3 ⊢ ∀𝑥(∃𝑎∃𝑦∀𝑧(𝑧 ∈ 𝑦 ↔ (𝑧 ∈ 𝑥 ∧ 𝜑)) → ∃𝑦∀𝑧(𝑧 ∈ 𝑦 ↔ (𝑧 ∈ 𝑥 ∧ 𝜑)))
3		bj-eximcom 37438	. . . . 5 ⊢ (∃𝑎(∃𝑦∀𝑡(𝑡 ∈ 𝑦 ↔ ∃𝑧 ∈ 𝑥 ((𝜑 ∧ 𝑡 = 𝑧) ∨ (¬ 𝜑 ∧ 𝑡 = 𝑎))) → ∃𝑦∀𝑧(𝑧 ∈ 𝑦 ↔ (𝑧 ∈ 𝑥 ∧ 𝜑))) → (∀𝑎∃𝑦∀𝑡(𝑡 ∈ 𝑦 ↔ ∃𝑧 ∈ 𝑥 ((𝜑 ∧ 𝑡 = 𝑧) ∨ (¬ 𝜑 ∧ 𝑡 = 𝑎))) → ∃𝑎∃𝑦∀𝑧(𝑧 ∈ 𝑦 ↔ (𝑧 ∈ 𝑥 ∧ 𝜑))))
4		bj-axseprep.axrep	. . . . . . . . 9 ⊢ ∀𝑥(∀𝑧 ∈ 𝑥 ∃!𝑡𝜓 → ∃𝑦∀𝑡(𝑡 ∈ 𝑦 ↔ ∃𝑧 ∈ 𝑥 𝜓))
5		bj-axseprep.ps	. . . . . . . . . . . . 13 ⊢ (𝜓 ↔ ((𝜑 ∧ 𝑡 = 𝑧) ∨ (¬ 𝜑 ∧ 𝑡 = 𝑎)))
6	5	eubii 2610	. . . . . . . . . . . 12 ⊢ (∃!𝑡𝜓 ↔ ∃!𝑡((𝜑 ∧ 𝑡 = 𝑧) ∨ (¬ 𝜑 ∧ 𝑡 = 𝑎)))
7	6	ralbii 3108	. . . . . . . . . . 11 ⊢ (∀𝑧 ∈ 𝑥 ∃!𝑡𝜓 ↔ ∀𝑧 ∈ 𝑥 ∃!𝑡((𝜑 ∧ 𝑡 = 𝑧) ∨ (¬ 𝜑 ∧ 𝑡 = 𝑎)))
8	5	rexbii 3109	. . . . . . . . . . . . . 14 ⊢ (∃𝑧 ∈ 𝑥 𝜓 ↔ ∃𝑧 ∈ 𝑥 ((𝜑 ∧ 𝑡 = 𝑧) ∨ (¬ 𝜑 ∧ 𝑡 = 𝑎)))
9	8	bibi2i 340	. . . . . . . . . . . . 13 ⊢ ((𝑡 ∈ 𝑦 ↔ ∃𝑧 ∈ 𝑥 𝜓) ↔ (𝑡 ∈ 𝑦 ↔ ∃𝑧 ∈ 𝑥 ((𝜑 ∧ 𝑡 = 𝑧) ∨ (¬ 𝜑 ∧ 𝑡 = 𝑎))))
10	9	albii 1852	. . . . . . . . . . . 12 ⊢ (∀𝑡(𝑡 ∈ 𝑦 ↔ ∃𝑧 ∈ 𝑥 𝜓) ↔ ∀𝑡(𝑡 ∈ 𝑦 ↔ ∃𝑧 ∈ 𝑥 ((𝜑 ∧ 𝑡 = 𝑧) ∨ (¬ 𝜑 ∧ 𝑡 = 𝑎))))
11	10	exbii 1881	. . . . . . . . . . 11 ⊢ (∃𝑦∀𝑡(𝑡 ∈ 𝑦 ↔ ∃𝑧 ∈ 𝑥 𝜓) ↔ ∃𝑦∀𝑡(𝑡 ∈ 𝑦 ↔ ∃𝑧 ∈ 𝑥 ((𝜑 ∧ 𝑡 = 𝑧) ∨ (¬ 𝜑 ∧ 𝑡 = 𝑎))))
12	7, 11	imbi12i 353	. . . . . . . . . 10 ⊢ ((∀𝑧 ∈ 𝑥 ∃!𝑡𝜓 → ∃𝑦∀𝑡(𝑡 ∈ 𝑦 ↔ ∃𝑧 ∈ 𝑥 𝜓)) ↔ (∀𝑧 ∈ 𝑥 ∃!𝑡((𝜑 ∧ 𝑡 = 𝑧) ∨ (¬ 𝜑 ∧ 𝑡 = 𝑎)) → ∃𝑦∀𝑡(𝑡 ∈ 𝑦 ↔ ∃𝑧 ∈ 𝑥 ((𝜑 ∧ 𝑡 = 𝑧) ∨ (¬ 𝜑 ∧ 𝑡 = 𝑎)))))
13	12	albii 1852	. . . . . . . . 9 ⊢ (∀𝑥(∀𝑧 ∈ 𝑥 ∃!𝑡𝜓 → ∃𝑦∀𝑡(𝑡 ∈ 𝑦 ↔ ∃𝑧 ∈ 𝑥 𝜓)) ↔ ∀𝑥(∀𝑧 ∈ 𝑥 ∃!𝑡((𝜑 ∧ 𝑡 = 𝑧) ∨ (¬ 𝜑 ∧ 𝑡 = 𝑎)) → ∃𝑦∀𝑡(𝑡 ∈ 𝑦 ↔ ∃𝑧 ∈ 𝑥 ((𝜑 ∧ 𝑡 = 𝑧) ∨ (¬ 𝜑 ∧ 𝑡 = 𝑎)))))
14	4, 13	mpbi 233	. . . . . . . 8 ⊢ ∀𝑥(∀𝑧 ∈ 𝑥 ∃!𝑡((𝜑 ∧ 𝑡 = 𝑧) ∨ (¬ 𝜑 ∧ 𝑡 = 𝑎)) → ∃𝑦∀𝑡(𝑡 ∈ 𝑦 ↔ ∃𝑧 ∈ 𝑥 ((𝜑 ∧ 𝑡 = 𝑧) ∨ (¬ 𝜑 ∧ 𝑡 = 𝑎))))
15		vex 3454	. . . . . . . . . . 11 ⊢ 𝑧 ∈ V
16		vex 3454	. . . . . . . . . . 11 ⊢ 𝑎 ∈ V
17	15, 16	eueq2 3667	. . . . . . . . . 10 ⊢ ∃!𝑡((𝜑 ∧ 𝑡 = 𝑧) ∨ (¬ 𝜑 ∧ 𝑡 = 𝑎))
18	17	rgenw 3080	. . . . . . . . 9 ⊢ ∀𝑧 ∈ 𝑥 ∃!𝑡((𝜑 ∧ 𝑡 = 𝑧) ∨ (¬ 𝜑 ∧ 𝑡 = 𝑎))
19	18	ax-gen 1828	. . . . . . . 8 ⊢ ∀𝑥∀𝑧 ∈ 𝑥 ∃!𝑡((𝜑 ∧ 𝑡 = 𝑧) ∨ (¬ 𝜑 ∧ 𝑡 = 𝑎))
20	14, 19	bj-almp 37403	. . . . . . 7 ⊢ ∀𝑥∃𝑦∀𝑡(𝑡 ∈ 𝑦 ↔ ∃𝑧 ∈ 𝑥 ((𝜑 ∧ 𝑡 = 𝑧) ∨ (¬ 𝜑 ∧ 𝑡 = 𝑎)))
21	20	ax-gen 1828	. . . . . 6 ⊢ ∀𝑎∀𝑥∃𝑦∀𝑡(𝑡 ∈ 𝑦 ↔ ∃𝑧 ∈ 𝑥 ((𝜑 ∧ 𝑡 = 𝑧) ∨ (¬ 𝜑 ∧ 𝑡 = 𝑎)))
22		alcom 2196	. . . . . 6 ⊢ (∀𝑎∀𝑥∃𝑦∀𝑡(𝑡 ∈ 𝑦 ↔ ∃𝑧 ∈ 𝑥 ((𝜑 ∧ 𝑡 = 𝑧) ∨ (¬ 𝜑 ∧ 𝑡 = 𝑎))) ↔ ∀𝑥∀𝑎∃𝑦∀𝑡(𝑡 ∈ 𝑦 ↔ ∃𝑧 ∈ 𝑥 ((𝜑 ∧ 𝑡 = 𝑧) ∨ (¬ 𝜑 ∧ 𝑡 = 𝑎))))
23	21, 22	mpbi 233	. . . . 5 ⊢ ∀𝑥∀𝑎∃𝑦∀𝑡(𝑡 ∈ 𝑦 ↔ ∃𝑧 ∈ 𝑥 ((𝜑 ∧ 𝑡 = 𝑧) ∨ (¬ 𝜑 ∧ 𝑡 = 𝑎)))
24	3, 23	bj-almpig 37412	. . . 4 ⊢ ∀𝑥(∃𝑎(∃𝑦∀𝑡(𝑡 ∈ 𝑦 ↔ ∃𝑧 ∈ 𝑥 ((𝜑 ∧ 𝑡 = 𝑧) ∨ (¬ 𝜑 ∧ 𝑡 = 𝑎))) → ∃𝑦∀𝑧(𝑧 ∈ 𝑦 ↔ (𝑧 ∈ 𝑥 ∧ 𝜑))) → ∃𝑎∃𝑦∀𝑧(𝑧 ∈ 𝑦 ↔ (𝑧 ∈ 𝑥 ∧ 𝜑)))
25		df-rex 3087	. . . . . . 7 ⊢ (∃𝑧 ∈ 𝑥 𝜑 ↔ ∃𝑧(𝑧 ∈ 𝑥 ∧ 𝜑))
26		nfv 1947	. . . . . . . 8 ⊢ Ⅎ𝑎(𝑧 ∈ 𝑥 ∧ 𝜑)
27	26	sb8ef 2384	. . . . . . 7 ⊢ (∃𝑧(𝑧 ∈ 𝑥 ∧ 𝜑) ↔ ∃𝑎[𝑎 / 𝑧](𝑧 ∈ 𝑥 ∧ 𝜑))
28	25, 27	bitri 278	. . . . . 6 ⊢ (∃𝑧 ∈ 𝑥 𝜑 ↔ ∃𝑎[𝑎 / 𝑧](𝑧 ∈ 𝑥 ∧ 𝜑))
29		df-rex 3087	. . . . . . . . . . . . . 14 ⊢ (∃𝑧 ∈ 𝑥 ((𝜑 ∧ 𝑡 = 𝑧) ∨ (¬ 𝜑 ∧ 𝑡 = 𝑎)) ↔ ∃𝑧(𝑧 ∈ 𝑥 ∧ ((𝜑 ∧ 𝑡 = 𝑧) ∨ (¬ 𝜑 ∧ 𝑡 = 𝑎))))
30		andi 1025	. . . . . . . . . . . . . . 15 ⊢ ((𝑧 ∈ 𝑥 ∧ ((𝜑 ∧ 𝑡 = 𝑧) ∨ (¬ 𝜑 ∧ 𝑡 = 𝑎))) ↔ ((𝑧 ∈ 𝑥 ∧ (𝜑 ∧ 𝑡 = 𝑧)) ∨ (𝑧 ∈ 𝑥 ∧ (¬ 𝜑 ∧ 𝑡 = 𝑎))))
31	30	exbii 1881	. . . . . . . . . . . . . 14 ⊢ (∃𝑧(𝑧 ∈ 𝑥 ∧ ((𝜑 ∧ 𝑡 = 𝑧) ∨ (¬ 𝜑 ∧ 𝑡 = 𝑎))) ↔ ∃𝑧((𝑧 ∈ 𝑥 ∧ (𝜑 ∧ 𝑡 = 𝑧)) ∨ (𝑧 ∈ 𝑥 ∧ (¬ 𝜑 ∧ 𝑡 = 𝑎))))
32		19.43 1915	. . . . . . . . . . . . . 14 ⊢ (∃𝑧((𝑧 ∈ 𝑥 ∧ (𝜑 ∧ 𝑡 = 𝑧)) ∨ (𝑧 ∈ 𝑥 ∧ (¬ 𝜑 ∧ 𝑡 = 𝑎))) ↔ (∃𝑧(𝑧 ∈ 𝑥 ∧ (𝜑 ∧ 𝑡 = 𝑧)) ∨ ∃𝑧(𝑧 ∈ 𝑥 ∧ (¬ 𝜑 ∧ 𝑡 = 𝑎))))
33	29, 31, 32	3bitri 300	. . . . . . . . . . . . 13 ⊢ (∃𝑧 ∈ 𝑥 ((𝜑 ∧ 𝑡 = 𝑧) ∨ (¬ 𝜑 ∧ 𝑡 = 𝑎)) ↔ (∃𝑧(𝑧 ∈ 𝑥 ∧ (𝜑 ∧ 𝑡 = 𝑧)) ∨ ∃𝑧(𝑧 ∈ 𝑥 ∧ (¬ 𝜑 ∧ 𝑡 = 𝑎))))
34		equcom 2051	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑧 = 𝑡 ↔ 𝑡 = 𝑧)
35	34	anbi1i 636	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑧 = 𝑡 ∧ (𝑧 ∈ 𝑥 ∧ 𝜑)) ↔ (𝑡 = 𝑧 ∧ (𝑧 ∈ 𝑥 ∧ 𝜑)))
36		ancom 466	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑡 = 𝑧 ∧ (𝑧 ∈ 𝑥 ∧ 𝜑)) ↔ ((𝑧 ∈ 𝑥 ∧ 𝜑) ∧ 𝑡 = 𝑧))
37		anass 474	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝑧 ∈ 𝑥 ∧ 𝜑) ∧ 𝑡 = 𝑧) ↔ (𝑧 ∈ 𝑥 ∧ (𝜑 ∧ 𝑡 = 𝑧)))
38	35, 36, 37	3bitri 300	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑧 = 𝑡 ∧ (𝑧 ∈ 𝑥 ∧ 𝜑)) ↔ (𝑧 ∈ 𝑥 ∧ (𝜑 ∧ 𝑡 = 𝑧)))
39	38	exbii 1881	. . . . . . . . . . . . . . . . 17 ⊢ (∃𝑧(𝑧 = 𝑡 ∧ (𝑧 ∈ 𝑥 ∧ 𝜑)) ↔ ∃𝑧(𝑧 ∈ 𝑥 ∧ (𝜑 ∧ 𝑡 = 𝑧)))
40	39	biimpri 231	. . . . . . . . . . . . . . . 16 ⊢ (∃𝑧(𝑧 ∈ 𝑥 ∧ (𝜑 ∧ 𝑡 = 𝑧)) → ∃𝑧(𝑧 = 𝑡 ∧ (𝑧 ∈ 𝑥 ∧ 𝜑)))
41	40	a1i 11	. . . . . . . . . . . . . . 15 ⊢ ([𝑎 / 𝑧](𝑧 ∈ 𝑥 ∧ 𝜑) → (∃𝑧(𝑧 ∈ 𝑥 ∧ (𝜑 ∧ 𝑡 = 𝑧)) → ∃𝑧(𝑧 = 𝑡 ∧ (𝑧 ∈ 𝑥 ∧ 𝜑))))
42		simprr 785	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑧 ∈ 𝑥 ∧ (¬ 𝜑 ∧ 𝑡 = 𝑎)) → 𝑡 = 𝑎)
43	42	exlimiv 1963	. . . . . . . . . . . . . . . 16 ⊢ (∃𝑧(𝑧 ∈ 𝑥 ∧ (¬ 𝜑 ∧ 𝑡 = 𝑎)) → 𝑡 = 𝑎)
44		sbequ 2120	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑎 = 𝑡 → ([𝑎 / 𝑧](𝑧 ∈ 𝑥 ∧ 𝜑) ↔ [𝑡 / 𝑧](𝑧 ∈ 𝑥 ∧ 𝜑)))
45	44	biimpd 232	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑎 = 𝑡 → ([𝑎 / 𝑧](𝑧 ∈ 𝑥 ∧ 𝜑) → [𝑡 / 𝑧](𝑧 ∈ 𝑥 ∧ 𝜑)))
46	45	equcoms 2053	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑡 = 𝑎 → ([𝑎 / 𝑧](𝑧 ∈ 𝑥 ∧ 𝜑) → [𝑡 / 𝑧](𝑧 ∈ 𝑥 ∧ 𝜑)))
47	46	com12 33	. . . . . . . . . . . . . . . . 17 ⊢ ([𝑎 / 𝑧](𝑧 ∈ 𝑥 ∧ 𝜑) → (𝑡 = 𝑎 → [𝑡 / 𝑧](𝑧 ∈ 𝑥 ∧ 𝜑)))
48		sb5 2309	. . . . . . . . . . . . . . . . 17 ⊢ ([𝑡 / 𝑧](𝑧 ∈ 𝑥 ∧ 𝜑) ↔ ∃𝑧(𝑧 = 𝑡 ∧ (𝑧 ∈ 𝑥 ∧ 𝜑)))
49	47, 48	imbitrdi 254	. . . . . . . . . . . . . . . 16 ⊢ ([𝑎 / 𝑧](𝑧 ∈ 𝑥 ∧ 𝜑) → (𝑡 = 𝑎 → ∃𝑧(𝑧 = 𝑡 ∧ (𝑧 ∈ 𝑥 ∧ 𝜑))))
50	43, 49	syl5 35	. . . . . . . . . . . . . . 15 ⊢ ([𝑎 / 𝑧](𝑧 ∈ 𝑥 ∧ 𝜑) → (∃𝑧(𝑧 ∈ 𝑥 ∧ (¬ 𝜑 ∧ 𝑡 = 𝑎)) → ∃𝑧(𝑧 = 𝑡 ∧ (𝑧 ∈ 𝑥 ∧ 𝜑))))
51	41, 50	jaod 873	. . . . . . . . . . . . . 14 ⊢ ([𝑎 / 𝑧](𝑧 ∈ 𝑥 ∧ 𝜑) → ((∃𝑧(𝑧 ∈ 𝑥 ∧ (𝜑 ∧ 𝑡 = 𝑧)) ∨ ∃𝑧(𝑧 ∈ 𝑥 ∧ (¬ 𝜑 ∧ 𝑡 = 𝑎))) → ∃𝑧(𝑧 = 𝑡 ∧ (𝑧 ∈ 𝑥 ∧ 𝜑))))
52		orc 881	. . . . . . . . . . . . . . 15 ⊢ (∃𝑧(𝑧 ∈ 𝑥 ∧ (𝜑 ∧ 𝑡 = 𝑧)) → (∃𝑧(𝑧 ∈ 𝑥 ∧ (𝜑 ∧ 𝑡 = 𝑧)) ∨ ∃𝑧(𝑧 ∈ 𝑥 ∧ (¬ 𝜑 ∧ 𝑡 = 𝑎))))
53	39, 52	sylbi 220	. . . . . . . . . . . . . 14 ⊢ (∃𝑧(𝑧 = 𝑡 ∧ (𝑧 ∈ 𝑥 ∧ 𝜑)) → (∃𝑧(𝑧 ∈ 𝑥 ∧ (𝜑 ∧ 𝑡 = 𝑧)) ∨ ∃𝑧(𝑧 ∈ 𝑥 ∧ (¬ 𝜑 ∧ 𝑡 = 𝑎))))
54	51, 53	impbid1 228	. . . . . . . . . . . . 13 ⊢ ([𝑎 / 𝑧](𝑧 ∈ 𝑥 ∧ 𝜑) → ((∃𝑧(𝑧 ∈ 𝑥 ∧ (𝜑 ∧ 𝑡 = 𝑧)) ∨ ∃𝑧(𝑧 ∈ 𝑥 ∧ (¬ 𝜑 ∧ 𝑡 = 𝑎))) ↔ ∃𝑧(𝑧 = 𝑡 ∧ (𝑧 ∈ 𝑥 ∧ 𝜑))))
55	33, 54	bitrid 286	. . . . . . . . . . . 12 ⊢ ([𝑎 / 𝑧](𝑧 ∈ 𝑥 ∧ 𝜑) → (∃𝑧 ∈ 𝑥 ((𝜑 ∧ 𝑡 = 𝑧) ∨ (¬ 𝜑 ∧ 𝑡 = 𝑎)) ↔ ∃𝑧(𝑧 = 𝑡 ∧ (𝑧 ∈ 𝑥 ∧ 𝜑))))
56	55	bibi2d 345	. . . . . . . . . . 11 ⊢ ([𝑎 / 𝑧](𝑧 ∈ 𝑥 ∧ 𝜑) → ((𝑡 ∈ 𝑦 ↔ ∃𝑧 ∈ 𝑥 ((𝜑 ∧ 𝑡 = 𝑧) ∨ (¬ 𝜑 ∧ 𝑡 = 𝑎))) ↔ (𝑡 ∈ 𝑦 ↔ ∃𝑧(𝑧 = 𝑡 ∧ (𝑧 ∈ 𝑥 ∧ 𝜑)))))
57	56	biimpd 232	. . . . . . . . . 10 ⊢ ([𝑎 / 𝑧](𝑧 ∈ 𝑥 ∧ 𝜑) → ((𝑡 ∈ 𝑦 ↔ ∃𝑧 ∈ 𝑥 ((𝜑 ∧ 𝑡 = 𝑧) ∨ (¬ 𝜑 ∧ 𝑡 = 𝑎))) → (𝑡 ∈ 𝑦 ↔ ∃𝑧(𝑧 = 𝑡 ∧ (𝑧 ∈ 𝑥 ∧ 𝜑)))))
58	57	alimdv 1949	. . . . . . . . 9 ⊢ ([𝑎 / 𝑧](𝑧 ∈ 𝑥 ∧ 𝜑) → (∀𝑡(𝑡 ∈ 𝑦 ↔ ∃𝑧 ∈ 𝑥 ((𝜑 ∧ 𝑡 = 𝑧) ∨ (¬ 𝜑 ∧ 𝑡 = 𝑎))) → ∀𝑡(𝑡 ∈ 𝑦 ↔ ∃𝑧(𝑧 = 𝑡 ∧ (𝑧 ∈ 𝑥 ∧ 𝜑)))))
59		nfv 1947	. . . . . . . . . . 11 ⊢ Ⅎ𝑧 𝑡 ∈ 𝑦
60		nfe1 2187	. . . . . . . . . . 11 ⊢ Ⅎ𝑧∃𝑧(𝑧 = 𝑡 ∧ (𝑧 ∈ 𝑥 ∧ 𝜑))
61	59, 60	nfbi 1936	. . . . . . . . . 10 ⊢ Ⅎ𝑧(𝑡 ∈ 𝑦 ↔ ∃𝑧(𝑧 = 𝑡 ∧ (𝑧 ∈ 𝑥 ∧ 𝜑)))
62		nfv 1947	. . . . . . . . . 10 ⊢ Ⅎ𝑡(𝑧 ∈ 𝑦 ↔ (𝑧 ∈ 𝑥 ∧ 𝜑))
63		elequ1 2152	. . . . . . . . . . 11 ⊢ (𝑡 = 𝑧 → (𝑡 ∈ 𝑦 ↔ 𝑧 ∈ 𝑦))
64	48	bicomi 227	. . . . . . . . . . . 12 ⊢ (∃𝑧(𝑧 = 𝑡 ∧ (𝑧 ∈ 𝑥 ∧ 𝜑)) ↔ [𝑡 / 𝑧](𝑧 ∈ 𝑥 ∧ 𝜑))
65		sbequ12r 2287	. . . . . . . . . . . 12 ⊢ (𝑡 = 𝑧 → ([𝑡 / 𝑧](𝑧 ∈ 𝑥 ∧ 𝜑) ↔ (𝑧 ∈ 𝑥 ∧ 𝜑)))
66	64, 65	bitrid 286	. . . . . . . . . . 11 ⊢ (𝑡 = 𝑧 → (∃𝑧(𝑧 = 𝑡 ∧ (𝑧 ∈ 𝑥 ∧ 𝜑)) ↔ (𝑧 ∈ 𝑥 ∧ 𝜑)))
67	63, 66	bibi12d 348	. . . . . . . . . 10 ⊢ (𝑡 = 𝑧 → ((𝑡 ∈ 𝑦 ↔ ∃𝑧(𝑧 = 𝑡 ∧ (𝑧 ∈ 𝑥 ∧ 𝜑))) ↔ (𝑧 ∈ 𝑦 ↔ (𝑧 ∈ 𝑥 ∧ 𝜑))))
68	61, 62, 67	cbvalv1 2370	. . . . . . . . 9 ⊢ (∀𝑡(𝑡 ∈ 𝑦 ↔ ∃𝑧(𝑧 = 𝑡 ∧ (𝑧 ∈ 𝑥 ∧ 𝜑))) ↔ ∀𝑧(𝑧 ∈ 𝑦 ↔ (𝑧 ∈ 𝑥 ∧ 𝜑)))
69	58, 68	imbitrdi 254	. . . . . . . 8 ⊢ ([𝑎 / 𝑧](𝑧 ∈ 𝑥 ∧ 𝜑) → (∀𝑡(𝑡 ∈ 𝑦 ↔ ∃𝑧 ∈ 𝑥 ((𝜑 ∧ 𝑡 = 𝑧) ∨ (¬ 𝜑 ∧ 𝑡 = 𝑎))) → ∀𝑧(𝑧 ∈ 𝑦 ↔ (𝑧 ∈ 𝑥 ∧ 𝜑))))
70	69	eximdv 1950	. . . . . . 7 ⊢ ([𝑎 / 𝑧](𝑧 ∈ 𝑥 ∧ 𝜑) → (∃𝑦∀𝑡(𝑡 ∈ 𝑦 ↔ ∃𝑧 ∈ 𝑥 ((𝜑 ∧ 𝑡 = 𝑧) ∨ (¬ 𝜑 ∧ 𝑡 = 𝑎))) → ∃𝑦∀𝑧(𝑧 ∈ 𝑦 ↔ (𝑧 ∈ 𝑥 ∧ 𝜑))))
71	70	eximi 1868	. . . . . 6 ⊢ (∃𝑎[𝑎 / 𝑧](𝑧 ∈ 𝑥 ∧ 𝜑) → ∃𝑎(∃𝑦∀𝑡(𝑡 ∈ 𝑦 ↔ ∃𝑧 ∈ 𝑥 ((𝜑 ∧ 𝑡 = 𝑧) ∨ (¬ 𝜑 ∧ 𝑡 = 𝑎))) → ∃𝑦∀𝑧(𝑧 ∈ 𝑦 ↔ (𝑧 ∈ 𝑥 ∧ 𝜑))))
72	28, 71	sylbi 220	. . . . 5 ⊢ (∃𝑧 ∈ 𝑥 𝜑 → ∃𝑎(∃𝑦∀𝑡(𝑡 ∈ 𝑦 ↔ ∃𝑧 ∈ 𝑥 ((𝜑 ∧ 𝑡 = 𝑧) ∨ (¬ 𝜑 ∧ 𝑡 = 𝑎))) → ∃𝑦∀𝑧(𝑧 ∈ 𝑦 ↔ (𝑧 ∈ 𝑥 ∧ 𝜑))))
73	72	ax-gen 1828	. . . 4 ⊢ ∀𝑥(∃𝑧 ∈ 𝑥 𝜑 → ∃𝑎(∃𝑦∀𝑡(𝑡 ∈ 𝑦 ↔ ∃𝑧 ∈ 𝑥 ((𝜑 ∧ 𝑡 = 𝑧) ∨ (¬ 𝜑 ∧ 𝑡 = 𝑎))) → ∃𝑦∀𝑧(𝑧 ∈ 𝑦 ↔ (𝑧 ∈ 𝑥 ∧ 𝜑))))
74	24, 73	barbara 2687	. . 3 ⊢ ∀𝑥(∃𝑧 ∈ 𝑥 𝜑 → ∃𝑎∃𝑦∀𝑧(𝑧 ∈ 𝑦 ↔ (𝑧 ∈ 𝑥 ∧ 𝜑)))
75	2, 74	barbara 2687	. 2 ⊢ ∀𝑥(∃𝑧 ∈ 𝑥 𝜑 → ∃𝑦∀𝑧(𝑧 ∈ 𝑦 ↔ (𝑧 ∈ 𝑥 ∧ 𝜑)))
76		ralnex 3088	. . . . 5 ⊢ (∀𝑧 ∈ 𝑥 ¬ 𝜑 ↔ ¬ ∃𝑧 ∈ 𝑥 𝜑)
77		df-ral 3077	. . . . . 6 ⊢ (∀𝑧 ∈ 𝑥 ¬ 𝜑 ↔ ∀𝑧(𝑧 ∈ 𝑥 → ¬ 𝜑))
78		df-ral 3077	. . . . . . 7 ⊢ (∀𝑧 ∈ 𝑦 ⊥ ↔ ∀𝑧(𝑧 ∈ 𝑦 → ⊥))
79		dfnot 1589	. . . . . . . . . . 11 ⊢ (¬ 𝑧 ∈ 𝑦 ↔ (𝑧 ∈ 𝑦 → ⊥))
80	79	bicomi 227	. . . . . . . . . 10 ⊢ ((𝑧 ∈ 𝑦 → ⊥) ↔ ¬ 𝑧 ∈ 𝑦)
81		imnan 405	. . . . . . . . . 10 ⊢ ((𝑧 ∈ 𝑥 → ¬ 𝜑) ↔ ¬ (𝑧 ∈ 𝑥 ∧ 𝜑))
82		pm5.21 837	. . . . . . . . . 10 ⊢ ((¬ 𝑧 ∈ 𝑦 ∧ ¬ (𝑧 ∈ 𝑥 ∧ 𝜑)) → (𝑧 ∈ 𝑦 ↔ (𝑧 ∈ 𝑥 ∧ 𝜑)))
83	80, 81, 82	syl2anb 610	. . . . . . . . 9 ⊢ (((𝑧 ∈ 𝑦 → ⊥) ∧ (𝑧 ∈ 𝑥 → ¬ 𝜑)) → (𝑧 ∈ 𝑦 ↔ (𝑧 ∈ 𝑥 ∧ 𝜑)))
84	83	expcom 419	. . . . . . . 8 ⊢ ((𝑧 ∈ 𝑥 → ¬ 𝜑) → ((𝑧 ∈ 𝑦 → ⊥) → (𝑧 ∈ 𝑦 ↔ (𝑧 ∈ 𝑥 ∧ 𝜑))))
85	84	al2imi 1848	. . . . . . 7 ⊢ (∀𝑧(𝑧 ∈ 𝑥 → ¬ 𝜑) → (∀𝑧(𝑧 ∈ 𝑦 → ⊥) → ∀𝑧(𝑧 ∈ 𝑦 ↔ (𝑧 ∈ 𝑥 ∧ 𝜑))))
86	78, 85	biimtrid 245	. . . . . 6 ⊢ (∀𝑧(𝑧 ∈ 𝑥 → ¬ 𝜑) → (∀𝑧 ∈ 𝑦 ⊥ → ∀𝑧(𝑧 ∈ 𝑦 ↔ (𝑧 ∈ 𝑥 ∧ 𝜑))))
87	77, 86	sylbi 220	. . . . 5 ⊢ (∀𝑧 ∈ 𝑥 ¬ 𝜑 → (∀𝑧 ∈ 𝑦 ⊥ → ∀𝑧(𝑧 ∈ 𝑦 ↔ (𝑧 ∈ 𝑥 ∧ 𝜑))))
88	76, 87	sylbir 238	. . . 4 ⊢ (¬ ∃𝑧 ∈ 𝑥 𝜑 → (∀𝑧 ∈ 𝑦 ⊥ → ∀𝑧(𝑧 ∈ 𝑦 ↔ (𝑧 ∈ 𝑥 ∧ 𝜑))))
89	88	eximdv 1950	. . 3 ⊢ (¬ ∃𝑧 ∈ 𝑥 𝜑 → (∃𝑦∀𝑧 ∈ 𝑦 ⊥ → ∃𝑦∀𝑧(𝑧 ∈ 𝑦 ↔ (𝑧 ∈ 𝑥 ∧ 𝜑))))
90		bj-axseprep.axnulw	. . . 4 ⊢ (∃𝑥⊤ → ∃𝑦∀𝑧 ∈ 𝑦 ⊥)
91		bj-alextruim 37458	. . . 4 ⊢ (∀𝑥∃𝑦∀𝑧 ∈ 𝑦 ⊥ ↔ (∃𝑥⊤ → ∃𝑦∀𝑧 ∈ 𝑦 ⊥))
92	90, 91	mpbir 234	. . 3 ⊢ ∀𝑥∃𝑦∀𝑧 ∈ 𝑦 ⊥
93	89, 92	bj-almpig 37412	. 2 ⊢ ∀𝑥(¬ ∃𝑧 ∈ 𝑥 𝜑 → ∃𝑦∀𝑧(𝑧 ∈ 𝑦 ↔ (𝑧 ∈ 𝑥 ∧ 𝜑)))
94		pm2.61 194	. . 3 ⊢ ((∃𝑧 ∈ 𝑥 𝜑 → ∃𝑦∀𝑧(𝑧 ∈ 𝑦 ↔ (𝑧 ∈ 𝑥 ∧ 𝜑))) → ((¬ ∃𝑧 ∈ 𝑥 𝜑 → ∃𝑦∀𝑧(𝑧 ∈ 𝑦 ↔ (𝑧 ∈ 𝑥 ∧ 𝜑))) → ∃𝑦∀𝑧(𝑧 ∈ 𝑦 ↔ (𝑧 ∈ 𝑥 ∧ 𝜑))))
95	94	al2imi 1848	. 2 ⊢ (∀𝑥(∃𝑧 ∈ 𝑥 𝜑 → ∃𝑦∀𝑧(𝑧 ∈ 𝑦 ↔ (𝑧 ∈ 𝑥 ∧ 𝜑))) → (∀𝑥(¬ ∃𝑧 ∈ 𝑥 𝜑 → ∃𝑦∀𝑧(𝑧 ∈ 𝑦 ↔ (𝑧 ∈ 𝑥 ∧ 𝜑))) → ∀𝑥∃𝑦∀𝑧(𝑧 ∈ 𝑦 ↔ (𝑧 ∈ 𝑥 ∧ 𝜑))))
96	75, 93, 95	mp2 9	1 ⊢ ∀𝑥∃𝑦∀𝑧(𝑧 ∈ 𝑦 ↔ (𝑧 ∈ 𝑥 ∧ 𝜑))

This proof depends on syntax axioms:  ¬ wn 3   → wi 4   ↔ wb 209   ∧ wa 401   ∨ wo 861  ∀wal 1568   = wceq 1570  ⊤wtru 1571  ⊥wfal 1582  ∃wex 1812  [wsb 2099   ∈ wcel 2145  ∃!weu 2593  ∀wral 3076  ∃wrex 3086

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-10 2178  ax-11 2194  ax-12 2213  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-tru 1573  df-fal 1583  df-ex 1813  df-nf 1817  df-sb 2100  df-mo 2564  df-eu 2594  df-clab 2739  df-cleq 2752  df-clel 2835  df-ral 3077  df-rex 3087  df-v 3452

This theorem is used by: (None)