Theorem bj-axseprep 38181

Description: Axiom of separation (universal closure of ax-sep 5252) 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 2010) 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 2387 and sbequ12r 2291 and eueq2 3671) could be reworked to avoid it. Proof modifications should not introduce steps relying on a nonempty universe, like alrimiv 1962. (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 1947	. . . 4 ⊢ (∃𝑎∃𝑦∀𝑧(𝑧 ∈ 𝑦 ↔ (𝑧 ∈ 𝑥 ∧ 𝜑)) → ∃𝑦∀𝑧(𝑧 ∈ 𝑦 ↔ (𝑧 ∈ 𝑥 ∧ 𝜑)))
2	1	ax-gen 1828	. . 3 ⊢ ∀𝑥(∃𝑎∃𝑦∀𝑧(𝑧 ∈ 𝑦 ↔ (𝑧 ∈ 𝑥 ∧ 𝜑)) → ∃𝑦∀𝑧(𝑧 ∈ 𝑦 ↔ (𝑧 ∈ 𝑥 ∧ 𝜑)))
3		bj-eximcom 37694	. . . . 5 ⊢ (∃𝑎(∃𝑦∀𝑡(𝑡 ∈ 𝑦 ↔ ∃𝑧 ∈ 𝑥 ((𝜑 ∧ 𝑡 = 𝑧) ∨ (¬ 𝜑 ∧ 𝑡 = 𝑎))) → ∃𝑦∀𝑧(𝑧 ∈ 𝑦 ↔ (𝑧 ∈ 𝑥 ∧ 𝜑))) → (∀𝑎∃𝑦∀𝑡(𝑡 ∈ 𝑦 ↔ ∃𝑧 ∈ 𝑥 ((𝜑 ∧ 𝑡 = 𝑧) ∨ (¬ 𝜑 ∧ 𝑡 = 𝑎))) → ∃𝑎∃𝑦∀𝑧(𝑧 ∈ 𝑦 ↔ (𝑧 ∈ 𝑥 ∧ 𝜑))))
4		bj-axseprep.axrep	. . . . . . . . 9 ⊢ ∀𝑥(∀𝑧 ∈ 𝑥 ∃!𝑡𝜓 → ∃𝑦∀𝑡(𝑡 ∈ 𝑦 ↔ ∃𝑧 ∈ 𝑥 𝜓))
5		bj-axseprep.ps	. . . . . . . . . . . . 13 ⊢ (𝜓 ↔ ((𝜑 ∧ 𝑡 = 𝑧) ∨ (¬ 𝜑 ∧ 𝑡 = 𝑎)))
6	5	eubii 2613	. . . . . . . . . . . 12 ⊢ (∃!𝑡𝜓 ↔ ∃!𝑡((𝜑 ∧ 𝑡 = 𝑧) ∨ (¬ 𝜑 ∧ 𝑡 = 𝑎)))
7	6	ralbii 3112	. . . . . . . . . . 11 ⊢ (∀𝑧 ∈ 𝑥 ∃!𝑡𝜓 ↔ ∀𝑧 ∈ 𝑥 ∃!𝑡((𝜑 ∧ 𝑡 = 𝑧) ∨ (¬ 𝜑 ∧ 𝑡 = 𝑎)))
8	5	rexbii 3113	. . . . . . . . . . . . . 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 3458	. . . . . . . . . . 11 ⊢ 𝑧 ∈ V
16		vex 3458	. . . . . . . . . . 11 ⊢ 𝑎 ∈ V
17	15, 16	eueq2 3671	. . . . . . . . . 10 ⊢ ∃!𝑡((𝜑 ∧ 𝑡 = 𝑧) ∨ (¬ 𝜑 ∧ 𝑡 = 𝑎))
18	17	rgenw 3084	. . . . . . . . 9 ⊢ ∀𝑧 ∈ 𝑥 ∃!𝑡((𝜑 ∧ 𝑡 = 𝑧) ∨ (¬ 𝜑 ∧ 𝑡 = 𝑎))
19	18	ax-gen 1828	. . . . . . . 8 ⊢ ∀𝑥∀𝑧 ∈ 𝑥 ∃!𝑡((𝜑 ∧ 𝑡 = 𝑧) ∨ (¬ 𝜑 ∧ 𝑡 = 𝑎))
20	14, 19	bj-almp 37659	. . . . . . 7 ⊢ ∀𝑥∃𝑦∀𝑡(𝑡 ∈ 𝑦 ↔ ∃𝑧 ∈ 𝑥 ((𝜑 ∧ 𝑡 = 𝑧) ∨ (¬ 𝜑 ∧ 𝑡 = 𝑎)))
21	20	ax-gen 1828	. . . . . 6 ⊢ ∀𝑎∀𝑥∃𝑦∀𝑡(𝑡 ∈ 𝑦 ↔ ∃𝑧 ∈ 𝑥 ((𝜑 ∧ 𝑡 = 𝑧) ∨ (¬ 𝜑 ∧ 𝑡 = 𝑎)))
22		alcom 2199	. . . . . 6 ⊢ (∀𝑎∀𝑥∃𝑦∀𝑡(𝑡 ∈ 𝑦 ↔ ∃𝑧 ∈ 𝑥 ((𝜑 ∧ 𝑡 = 𝑧) ∨ (¬ 𝜑 ∧ 𝑡 = 𝑎))) ↔ ∀𝑥∀𝑎∃𝑦∀𝑡(𝑡 ∈ 𝑦 ↔ ∃𝑧 ∈ 𝑥 ((𝜑 ∧ 𝑡 = 𝑧) ∨ (¬ 𝜑 ∧ 𝑡 = 𝑎))))
23	21, 22	mpbi 233	. . . . 5 ⊢ ∀𝑥∀𝑎∃𝑦∀𝑡(𝑡 ∈ 𝑦 ↔ ∃𝑧 ∈ 𝑥 ((𝜑 ∧ 𝑡 = 𝑧) ∨ (¬ 𝜑 ∧ 𝑡 = 𝑎)))
24	3, 23	bj-almpig 37668	. . . 4 ⊢ ∀𝑥(∃𝑎(∃𝑦∀𝑡(𝑡 ∈ 𝑦 ↔ ∃𝑧 ∈ 𝑥 ((𝜑 ∧ 𝑡 = 𝑧) ∨ (¬ 𝜑 ∧ 𝑡 = 𝑎))) → ∃𝑦∀𝑧(𝑧 ∈ 𝑦 ↔ (𝑧 ∈ 𝑥 ∧ 𝜑))) → ∃𝑎∃𝑦∀𝑧(𝑧 ∈ 𝑦 ↔ (𝑧 ∈ 𝑥 ∧ 𝜑)))
25		df-rex 3091	. . . . . . 7 ⊢ (∃𝑧 ∈ 𝑥 𝜑 ↔ ∃𝑧(𝑧 ∈ 𝑥 ∧ 𝜑))
26		nfv 1949	. . . . . . . 8 ⊢ Ⅎ𝑎(𝑧 ∈ 𝑥 ∧ 𝜑)
27	26	sb8ef 2387	. . . . . . 7 ⊢ (∃𝑧(𝑧 ∈ 𝑥 ∧ 𝜑) ↔ ∃𝑎[𝑎 / 𝑧](𝑧 ∈ 𝑥 ∧ 𝜑))
28	25, 27	bitri 278	. . . . . 6 ⊢ (∃𝑧 ∈ 𝑥 𝜑 ↔ ∃𝑎[𝑎 / 𝑧](𝑧 ∈ 𝑥 ∧ 𝜑))
29		df-rex 3091	. . . . . . . . . . . . . 14 ⊢ (∃𝑧 ∈ 𝑥 ((𝜑 ∧ 𝑡 = 𝑧) ∨ (¬ 𝜑 ∧ 𝑡 = 𝑎)) ↔ ∃𝑧(𝑧 ∈ 𝑥 ∧ ((𝜑 ∧ 𝑡 = 𝑧) ∨ (¬ 𝜑 ∧ 𝑡 = 𝑎))))
30		andi 1025	. . . . . . . . . . . . . . 15 ⊢ ((𝑧 ∈ 𝑥 ∧ ((𝜑 ∧ 𝑡 = 𝑧) ∨ (¬ 𝜑 ∧ 𝑡 = 𝑎))) ↔ ((𝑧 ∈ 𝑥 ∧ (𝜑 ∧ 𝑡 = 𝑧)) ∨ (𝑧 ∈ 𝑥 ∧ (¬ 𝜑 ∧ 𝑡 = 𝑎))))
31	30	exbii 1881	. . . . . . . . . . . . . 14 ⊢ (∃𝑧(𝑧 ∈ 𝑥 ∧ ((𝜑 ∧ 𝑡 = 𝑧) ∨ (¬ 𝜑 ∧ 𝑡 = 𝑎))) ↔ ∃𝑧((𝑧 ∈ 𝑥 ∧ (𝜑 ∧ 𝑡 = 𝑧)) ∨ (𝑧 ∈ 𝑥 ∧ (¬ 𝜑 ∧ 𝑡 = 𝑎))))
32		19.43 1917	. . . . . . . . . . . . . 14 ⊢ (∃𝑧((𝑧 ∈ 𝑥 ∧ (𝜑 ∧ 𝑡 = 𝑧)) ∨ (𝑧 ∈ 𝑥 ∧ (¬ 𝜑 ∧ 𝑡 = 𝑎))) ↔ (∃𝑧(𝑧 ∈ 𝑥 ∧ (𝜑 ∧ 𝑡 = 𝑧)) ∨ ∃𝑧(𝑧 ∈ 𝑥 ∧ (¬ 𝜑 ∧ 𝑡 = 𝑎))))
33	29, 31, 32	3bitri 300	. . . . . . . . . . . . 13 ⊢ (∃𝑧 ∈ 𝑥 ((𝜑 ∧ 𝑡 = 𝑧) ∨ (¬ 𝜑 ∧ 𝑡 = 𝑎)) ↔ (∃𝑧(𝑧 ∈ 𝑥 ∧ (𝜑 ∧ 𝑡 = 𝑧)) ∨ ∃𝑧(𝑧 ∈ 𝑥 ∧ (¬ 𝜑 ∧ 𝑡 = 𝑎))))
34		equcom 2053	. . . . . . . . . . . . . . . . . . . 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 1965	. . . . . . . . . . . . . . . 16 ⊢ (∃𝑧(𝑧 ∈ 𝑥 ∧ (¬ 𝜑 ∧ 𝑡 = 𝑎)) → 𝑡 = 𝑎)
44		sbequ 2122	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑎 = 𝑡 → ([𝑎 / 𝑧](𝑧 ∈ 𝑥 ∧ 𝜑) ↔ [𝑡 / 𝑧](𝑧 ∈ 𝑥 ∧ 𝜑)))
45	44	biimpd 232	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑎 = 𝑡 → ([𝑎 / 𝑧](𝑧 ∈ 𝑥 ∧ 𝜑) → [𝑡 / 𝑧](𝑧 ∈ 𝑥 ∧ 𝜑)))
46	45	equcoms 2055	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑡 = 𝑎 → ([𝑎 / 𝑧](𝑧 ∈ 𝑥 ∧ 𝜑) → [𝑡 / 𝑧](𝑧 ∈ 𝑥 ∧ 𝜑)))
47	46	com12 33	. . . . . . . . . . . . . . . . 17 ⊢ ([𝑎 / 𝑧](𝑧 ∈ 𝑥 ∧ 𝜑) → (𝑡 = 𝑎 → [𝑡 / 𝑧](𝑧 ∈ 𝑥 ∧ 𝜑)))
48		sb5 2313	. . . . . . . . . . . . . . . . 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 1951	. . . . . . . . 9 ⊢ ([𝑎 / 𝑧](𝑧 ∈ 𝑥 ∧ 𝜑) → (∀𝑡(𝑡 ∈ 𝑦 ↔ ∃𝑧 ∈ 𝑥 ((𝜑 ∧ 𝑡 = 𝑧) ∨ (¬ 𝜑 ∧ 𝑡 = 𝑎))) → ∀𝑡(𝑡 ∈ 𝑦 ↔ ∃𝑧(𝑧 = 𝑡 ∧ (𝑧 ∈ 𝑥 ∧ 𝜑)))))
59		nfv 1949	. . . . . . . . . . 11 ⊢ Ⅎ𝑧 𝑡 ∈ 𝑦
60		nfe1 2190	. . . . . . . . . . 11 ⊢ Ⅎ𝑧∃𝑧(𝑧 = 𝑡 ∧ (𝑧 ∈ 𝑥 ∧ 𝜑))
61	59, 60	nfbi 1938	. . . . . . . . . 10 ⊢ Ⅎ𝑧(𝑡 ∈ 𝑦 ↔ ∃𝑧(𝑧 = 𝑡 ∧ (𝑧 ∈ 𝑥 ∧ 𝜑)))
62		nfv 1949	. . . . . . . . . 10 ⊢ Ⅎ𝑡(𝑧 ∈ 𝑦 ↔ (𝑧 ∈ 𝑥 ∧ 𝜑))
63		elequ1 2154	. . . . . . . . . . 11 ⊢ (𝑡 = 𝑧 → (𝑡 ∈ 𝑦 ↔ 𝑧 ∈ 𝑦))
64	48	bicomi 227	. . . . . . . . . . . 12 ⊢ (∃𝑧(𝑧 = 𝑡 ∧ (𝑧 ∈ 𝑥 ∧ 𝜑)) ↔ [𝑡 / 𝑧](𝑧 ∈ 𝑥 ∧ 𝜑))
65		sbequ12r 2291	. . . . . . . . . . . 12 ⊢ (𝑡 = 𝑧 → ([𝑡 / 𝑧](𝑧 ∈ 𝑥 ∧ 𝜑) ↔ (𝑧 ∈ 𝑥 ∧ 𝜑)))
66	64, 65	bitrid 286	. . . . . . . . . . 11 ⊢ (𝑡 = 𝑧 → (∃𝑧(𝑧 = 𝑡 ∧ (𝑧 ∈ 𝑥 ∧ 𝜑)) ↔ (𝑧 ∈ 𝑥 ∧ 𝜑)))
67	63, 66	bibi12d 348	. . . . . . . . . 10 ⊢ (𝑡 = 𝑧 → ((𝑡 ∈ 𝑦 ↔ ∃𝑧(𝑧 = 𝑡 ∧ (𝑧 ∈ 𝑥 ∧ 𝜑))) ↔ (𝑧 ∈ 𝑦 ↔ (𝑧 ∈ 𝑥 ∧ 𝜑))))
68	61, 62, 67	cbvalv1 2374	. . . . . . . . 9 ⊢ (∀𝑡(𝑡 ∈ 𝑦 ↔ ∃𝑧(𝑧 = 𝑡 ∧ (𝑧 ∈ 𝑥 ∧ 𝜑))) ↔ ∀𝑧(𝑧 ∈ 𝑦 ↔ (𝑧 ∈ 𝑥 ∧ 𝜑)))
69	58, 68	imbitrdi 254	. . . . . . . 8 ⊢ ([𝑎 / 𝑧](𝑧 ∈ 𝑥 ∧ 𝜑) → (∀𝑡(𝑡 ∈ 𝑦 ↔ ∃𝑧 ∈ 𝑥 ((𝜑 ∧ 𝑡 = 𝑧) ∨ (¬ 𝜑 ∧ 𝑡 = 𝑎))) → ∀𝑧(𝑧 ∈ 𝑦 ↔ (𝑧 ∈ 𝑥 ∧ 𝜑))))
70	69	eximdv 1952	. . . . . . 7 ⊢ ([𝑎 / 𝑧](𝑧 ∈ 𝑥 ∧ 𝜑) → (∃𝑦∀𝑡(𝑡 ∈ 𝑦 ↔ ∃𝑧 ∈ 𝑥 ((𝜑 ∧ 𝑡 = 𝑧) ∨ (¬ 𝜑 ∧ 𝑡 = 𝑎))) → ∃𝑦∀𝑧(𝑧 ∈ 𝑦 ↔ (𝑧 ∈ 𝑥 ∧ 𝜑))))
71	70	eximi 1868	. . . . . 6 ⊢ (∃𝑎[𝑎 / 𝑧](𝑧 ∈ 𝑥 ∧ 𝜑) → ∃𝑎(∃𝑦∀𝑡(𝑡 ∈ 𝑦 ↔ ∃𝑧 ∈ 𝑥 ((𝜑 ∧ 𝑡 = 𝑧) ∨ (¬ 𝜑 ∧ 𝑡 = 𝑎))) → ∃𝑦∀𝑧(𝑧 ∈ 𝑦 ↔ (𝑧 ∈ 𝑥 ∧ 𝜑))))
72	28, 71	sylbi 220	. . . . 5 ⊢ (∃𝑧 ∈ 𝑥 𝜑 → ∃𝑎(∃𝑦∀𝑡(𝑡 ∈ 𝑦 ↔ ∃𝑧 ∈ 𝑥 ((𝜑 ∧ 𝑡 = 𝑧) ∨ (¬ 𝜑 ∧ 𝑡 = 𝑎))) → ∃𝑦∀𝑧(𝑧 ∈ 𝑦 ↔ (𝑧 ∈ 𝑥 ∧ 𝜑))))
73	72	ax-gen 1828	. . . 4 ⊢ ∀𝑥(∃𝑧 ∈ 𝑥 𝜑 → ∃𝑎(∃𝑦∀𝑡(𝑡 ∈ 𝑦 ↔ ∃𝑧 ∈ 𝑥 ((𝜑 ∧ 𝑡 = 𝑧) ∨ (¬ 𝜑 ∧ 𝑡 = 𝑎))) → ∃𝑦∀𝑧(𝑧 ∈ 𝑦 ↔ (𝑧 ∈ 𝑥 ∧ 𝜑))))
74	24, 73	barbara 2690	. . 3 ⊢ ∀𝑥(∃𝑧 ∈ 𝑥 𝜑 → ∃𝑎∃𝑦∀𝑧(𝑧 ∈ 𝑦 ↔ (𝑧 ∈ 𝑥 ∧ 𝜑)))
75	2, 74	barbara 2690	. 2 ⊢ ∀𝑥(∃𝑧 ∈ 𝑥 𝜑 → ∃𝑦∀𝑧(𝑧 ∈ 𝑦 ↔ (𝑧 ∈ 𝑥 ∧ 𝜑)))
76		ralnex 3092	. . . . 5 ⊢ (∀𝑧 ∈ 𝑥 ¬ 𝜑 ↔ ¬ ∃𝑧 ∈ 𝑥 𝜑)
77		df-ral 3081	. . . . . 6 ⊢ (∀𝑧 ∈ 𝑥 ¬ 𝜑 ↔ ∀𝑧(𝑧 ∈ 𝑥 → ¬ 𝜑))
78		df-ral 3081	. . . . . . 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 1952	. . 3 ⊢ (¬ ∃𝑧 ∈ 𝑥 𝜑 → (∃𝑦∀𝑧 ∈ 𝑦 ⊥ → ∃𝑦∀𝑧(𝑧 ∈ 𝑦 ↔ (𝑧 ∈ 𝑥 ∧ 𝜑))))
90		bj-axseprep.axnulw	. . . 4 ⊢ (∃𝑥⊤ → ∃𝑦∀𝑧 ∈ 𝑦 ⊥)
91		bj-alextruim 37714	. . . 4 ⊢ (∀𝑥∃𝑦∀𝑧 ∈ 𝑦 ⊥ ↔ (∃𝑥⊤ → ∃𝑦∀𝑧 ∈ 𝑦 ⊥))
92	90, 91	mpbir 234	. . 3 ⊢ ∀𝑥∃𝑦∀𝑧 ∈ 𝑦 ⊥
93	89, 92	bj-almpig 37668	. 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 2101   ∈ wcel 2147  ∃!weu 2596  ∀wral 3080  ∃wrex 3090

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 1945  ax-6 2002  ax-7 2043  ax-8 2149  ax-9 2157  ax-10 2180  ax-11 2197  ax-12 2216  ax-ext 2735

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 2102  df-mo 2567  df-eu 2597  df-clab 2742  df-cleq 2755  df-clel 2839  df-ral 3081  df-rex 3091  df-v 3456

This theorem is used by: (None)