Theorem bj-axseprep 37564

Description: Axiom of separation (universal closure of ax-sep 5247) 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 1996) 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 2288 and eueq2 3674) could be reworked to avoid it. Proof modifications should not introduce steps relying on a nonempty universe, like alrimiv 1948. (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 1933	. . . 4 ⊢ (∃𝑎∃𝑦∀𝑧(𝑧 ∈ 𝑦 ↔ (𝑧 ∈ 𝑥 ∧ 𝜑)) → ∃𝑦∀𝑧(𝑧 ∈ 𝑦 ↔ (𝑧 ∈ 𝑥 ∧ 𝜑)))
2	1	ax-gen 1816	. . 3 ⊢ ∀𝑥(∃𝑎∃𝑦∀𝑧(𝑧 ∈ 𝑦 ↔ (𝑧 ∈ 𝑥 ∧ 𝜑)) → ∃𝑦∀𝑧(𝑧 ∈ 𝑦 ↔ (𝑧 ∈ 𝑥 ∧ 𝜑)))
3		bj-eximcom 37094	. . . . 5 ⊢ (∃𝑎(∃𝑦∀𝑡(𝑡 ∈ 𝑦 ↔ ∃𝑧 ∈ 𝑥 ((𝜑 ∧ 𝑡 = 𝑧) ∨ (¬ 𝜑 ∧ 𝑡 = 𝑎))) → ∃𝑦∀𝑧(𝑧 ∈ 𝑦 ↔ (𝑧 ∈ 𝑥 ∧ 𝜑))) → (∀𝑎∃𝑦∀𝑡(𝑡 ∈ 𝑦 ↔ ∃𝑧 ∈ 𝑥 ((𝜑 ∧ 𝑡 = 𝑧) ∨ (¬ 𝜑 ∧ 𝑡 = 𝑎))) → ∃𝑎∃𝑦∀𝑧(𝑧 ∈ 𝑦 ↔ (𝑧 ∈ 𝑥 ∧ 𝜑))))
4		bj-axseprep.axrep	. . . . . . . . 9 ⊢ ∀𝑥(∀𝑧 ∈ 𝑥 ∃!𝑡𝜓 → ∃𝑦∀𝑡(𝑡 ∈ 𝑦 ↔ ∃𝑧 ∈ 𝑥 𝜓))
5		bj-axseprep.ps	. . . . . . . . . . . . 13 ⊢ (𝜓 ↔ ((𝜑 ∧ 𝑡 = 𝑧) ∨ (¬ 𝜑 ∧ 𝑡 = 𝑎)))
6	5	eubii 2613	. . . . . . . . . . . 12 ⊢ (∃!𝑡𝜓 ↔ ∃!𝑡((𝜑 ∧ 𝑡 = 𝑧) ∨ (¬ 𝜑 ∧ 𝑡 = 𝑎)))
7	6	ralbii 3109	. . . . . . . . . . 11 ⊢ (∀𝑧 ∈ 𝑥 ∃!𝑡𝜓 ↔ ∀𝑧 ∈ 𝑥 ∃!𝑡((𝜑 ∧ 𝑡 = 𝑧) ∨ (¬ 𝜑 ∧ 𝑡 = 𝑎)))
8	5	rexbii 3110	. . . . . . . . . . . . . 14 ⊢ (∃𝑧 ∈ 𝑥 𝜓 ↔ ∃𝑧 ∈ 𝑥 ((𝜑 ∧ 𝑡 = 𝑧) ∨ (¬ 𝜑 ∧ 𝑡 = 𝑎)))
9	8	bibi2i 339	. . . . . . . . . . . . 13 ⊢ ((𝑡 ∈ 𝑦 ↔ ∃𝑧 ∈ 𝑥 𝜓) ↔ (𝑡 ∈ 𝑦 ↔ ∃𝑧 ∈ 𝑥 ((𝜑 ∧ 𝑡 = 𝑧) ∨ (¬ 𝜑 ∧ 𝑡 = 𝑎))))
10	9	albii 1840	. . . . . . . . . . . 12 ⊢ (∀𝑡(𝑡 ∈ 𝑦 ↔ ∃𝑧 ∈ 𝑥 𝜓) ↔ ∀𝑡(𝑡 ∈ 𝑦 ↔ ∃𝑧 ∈ 𝑥 ((𝜑 ∧ 𝑡 = 𝑧) ∨ (¬ 𝜑 ∧ 𝑡 = 𝑎))))
11	10	exbii 1869	. . . . . . . . . . 11 ⊢ (∃𝑦∀𝑡(𝑡 ∈ 𝑦 ↔ ∃𝑧 ∈ 𝑥 𝜓) ↔ ∃𝑦∀𝑡(𝑡 ∈ 𝑦 ↔ ∃𝑧 ∈ 𝑥 ((𝜑 ∧ 𝑡 = 𝑧) ∨ (¬ 𝜑 ∧ 𝑡 = 𝑎))))
12	7, 11	imbi12i 352	. . . . . . . . . 10 ⊢ ((∀𝑧 ∈ 𝑥 ∃!𝑡𝜓 → ∃𝑦∀𝑡(𝑡 ∈ 𝑦 ↔ ∃𝑧 ∈ 𝑥 𝜓)) ↔ (∀𝑧 ∈ 𝑥 ∃!𝑡((𝜑 ∧ 𝑡 = 𝑧) ∨ (¬ 𝜑 ∧ 𝑡 = 𝑎)) → ∃𝑦∀𝑡(𝑡 ∈ 𝑦 ↔ ∃𝑧 ∈ 𝑥 ((𝜑 ∧ 𝑡 = 𝑧) ∨ (¬ 𝜑 ∧ 𝑡 = 𝑎)))))
13	12	albii 1840	. . . . . . . . 9 ⊢ (∀𝑥(∀𝑧 ∈ 𝑥 ∃!𝑡𝜓 → ∃𝑦∀𝑡(𝑡 ∈ 𝑦 ↔ ∃𝑧 ∈ 𝑥 𝜓)) ↔ ∀𝑥(∀𝑧 ∈ 𝑥 ∃!𝑡((𝜑 ∧ 𝑡 = 𝑧) ∨ (¬ 𝜑 ∧ 𝑡 = 𝑎)) → ∃𝑦∀𝑡(𝑡 ∈ 𝑦 ↔ ∃𝑧 ∈ 𝑥 ((𝜑 ∧ 𝑡 = 𝑧) ∨ (¬ 𝜑 ∧ 𝑡 = 𝑎)))))
14	4, 13	mpbi 232	. . . . . . . 8 ⊢ ∀𝑥(∀𝑧 ∈ 𝑥 ∃!𝑡((𝜑 ∧ 𝑡 = 𝑧) ∨ (¬ 𝜑 ∧ 𝑡 = 𝑎)) → ∃𝑦∀𝑡(𝑡 ∈ 𝑦 ↔ ∃𝑧 ∈ 𝑥 ((𝜑 ∧ 𝑡 = 𝑧) ∨ (¬ 𝜑 ∧ 𝑡 = 𝑎))))
15		vex 3459	. . . . . . . . . . 11 ⊢ 𝑧 ∈ V
16		vex 3459	. . . . . . . . . . 11 ⊢ 𝑎 ∈ V
17	15, 16	eueq2 3674	. . . . . . . . . 10 ⊢ ∃!𝑡((𝜑 ∧ 𝑡 = 𝑧) ∨ (¬ 𝜑 ∧ 𝑡 = 𝑎))
18	17	rgenw 3081	. . . . . . . . 9 ⊢ ∀𝑧 ∈ 𝑥 ∃!𝑡((𝜑 ∧ 𝑡 = 𝑧) ∨ (¬ 𝜑 ∧ 𝑡 = 𝑎))
19	18	ax-gen 1816	. . . . . . . 8 ⊢ ∀𝑥∀𝑧 ∈ 𝑥 ∃!𝑡((𝜑 ∧ 𝑡 = 𝑧) ∨ (¬ 𝜑 ∧ 𝑡 = 𝑎))
20	14, 19	bj-almp 37059	. . . . . . 7 ⊢ ∀𝑥∃𝑦∀𝑡(𝑡 ∈ 𝑦 ↔ ∃𝑧 ∈ 𝑥 ((𝜑 ∧ 𝑡 = 𝑧) ∨ (¬ 𝜑 ∧ 𝑡 = 𝑎)))
21	20	ax-gen 1816	. . . . . 6 ⊢ ∀𝑎∀𝑥∃𝑦∀𝑡(𝑡 ∈ 𝑦 ↔ ∃𝑧 ∈ 𝑥 ((𝜑 ∧ 𝑡 = 𝑧) ∨ (¬ 𝜑 ∧ 𝑡 = 𝑎)))
22		alcom 2194	. . . . . 6 ⊢ (∀𝑎∀𝑥∃𝑦∀𝑡(𝑡 ∈ 𝑦 ↔ ∃𝑧 ∈ 𝑥 ((𝜑 ∧ 𝑡 = 𝑧) ∨ (¬ 𝜑 ∧ 𝑡 = 𝑎))) ↔ ∀𝑥∀𝑎∃𝑦∀𝑡(𝑡 ∈ 𝑦 ↔ ∃𝑧 ∈ 𝑥 ((𝜑 ∧ 𝑡 = 𝑧) ∨ (¬ 𝜑 ∧ 𝑡 = 𝑎))))
23	21, 22	mpbi 232	. . . . 5 ⊢ ∀𝑥∀𝑎∃𝑦∀𝑡(𝑡 ∈ 𝑦 ↔ ∃𝑧 ∈ 𝑥 ((𝜑 ∧ 𝑡 = 𝑧) ∨ (¬ 𝜑 ∧ 𝑡 = 𝑎)))
24	3, 23	bj-almpig 37068	. . . 4 ⊢ ∀𝑥(∃𝑎(∃𝑦∀𝑡(𝑡 ∈ 𝑦 ↔ ∃𝑧 ∈ 𝑥 ((𝜑 ∧ 𝑡 = 𝑧) ∨ (¬ 𝜑 ∧ 𝑡 = 𝑎))) → ∃𝑦∀𝑧(𝑧 ∈ 𝑦 ↔ (𝑧 ∈ 𝑥 ∧ 𝜑))) → ∃𝑎∃𝑦∀𝑧(𝑧 ∈ 𝑦 ↔ (𝑧 ∈ 𝑥 ∧ 𝜑)))
25		df-rex 3088	. . . . . . 7 ⊢ (∃𝑧 ∈ 𝑥 𝜑 ↔ ∃𝑧(𝑧 ∈ 𝑥 ∧ 𝜑))
26		nfv 1935	. . . . . . . 8 ⊢ Ⅎ𝑎(𝑧 ∈ 𝑥 ∧ 𝜑)
27	26	sb8ef 2387	. . . . . . 7 ⊢ (∃𝑧(𝑧 ∈ 𝑥 ∧ 𝜑) ↔ ∃𝑎[𝑎 / 𝑧](𝑧 ∈ 𝑥 ∧ 𝜑))
28	25, 27	bitri 277	. . . . . 6 ⊢ (∃𝑧 ∈ 𝑥 𝜑 ↔ ∃𝑎[𝑎 / 𝑧](𝑧 ∈ 𝑥 ∧ 𝜑))
29		df-rex 3088	. . . . . . . . . . . . . 14 ⊢ (∃𝑧 ∈ 𝑥 ((𝜑 ∧ 𝑡 = 𝑧) ∨ (¬ 𝜑 ∧ 𝑡 = 𝑎)) ↔ ∃𝑧(𝑧 ∈ 𝑥 ∧ ((𝜑 ∧ 𝑡 = 𝑧) ∨ (¬ 𝜑 ∧ 𝑡 = 𝑎))))
30		andi 1021	. . . . . . . . . . . . . . 15 ⊢ ((𝑧 ∈ 𝑥 ∧ ((𝜑 ∧ 𝑡 = 𝑧) ∨ (¬ 𝜑 ∧ 𝑡 = 𝑎))) ↔ ((𝑧 ∈ 𝑥 ∧ (𝜑 ∧ 𝑡 = 𝑧)) ∨ (𝑧 ∈ 𝑥 ∧ (¬ 𝜑 ∧ 𝑡 = 𝑎))))
31	30	exbii 1869	. . . . . . . . . . . . . 14 ⊢ (∃𝑧(𝑧 ∈ 𝑥 ∧ ((𝜑 ∧ 𝑡 = 𝑧) ∨ (¬ 𝜑 ∧ 𝑡 = 𝑎))) ↔ ∃𝑧((𝑧 ∈ 𝑥 ∧ (𝜑 ∧ 𝑡 = 𝑧)) ∨ (𝑧 ∈ 𝑥 ∧ (¬ 𝜑 ∧ 𝑡 = 𝑎))))
32		19.43 1903	. . . . . . . . . . . . . 14 ⊢ (∃𝑧((𝑧 ∈ 𝑥 ∧ (𝜑 ∧ 𝑡 = 𝑧)) ∨ (𝑧 ∈ 𝑥 ∧ (¬ 𝜑 ∧ 𝑡 = 𝑎))) ↔ (∃𝑧(𝑧 ∈ 𝑥 ∧ (𝜑 ∧ 𝑡 = 𝑧)) ∨ ∃𝑧(𝑧 ∈ 𝑥 ∧ (¬ 𝜑 ∧ 𝑡 = 𝑎))))
33	29, 31, 32	3bitri 299	. . . . . . . . . . . . 13 ⊢ (∃𝑧 ∈ 𝑥 ((𝜑 ∧ 𝑡 = 𝑧) ∨ (¬ 𝜑 ∧ 𝑡 = 𝑎)) ↔ (∃𝑧(𝑧 ∈ 𝑥 ∧ (𝜑 ∧ 𝑡 = 𝑧)) ∨ ∃𝑧(𝑧 ∈ 𝑥 ∧ (¬ 𝜑 ∧ 𝑡 = 𝑎))))
34		equcom 2039	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑧 = 𝑡 ↔ 𝑡 = 𝑧)
35	34	anbi1i 633	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑧 = 𝑡 ∧ (𝑧 ∈ 𝑥 ∧ 𝜑)) ↔ (𝑡 = 𝑧 ∧ (𝑧 ∈ 𝑥 ∧ 𝜑)))
36		ancom 464	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑡 = 𝑧 ∧ (𝑧 ∈ 𝑥 ∧ 𝜑)) ↔ ((𝑧 ∈ 𝑥 ∧ 𝜑) ∧ 𝑡 = 𝑧))
37		anass 472	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝑧 ∈ 𝑥 ∧ 𝜑) ∧ 𝑡 = 𝑧) ↔ (𝑧 ∈ 𝑥 ∧ (𝜑 ∧ 𝑡 = 𝑧)))
38	35, 36, 37	3bitri 299	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑧 = 𝑡 ∧ (𝑧 ∈ 𝑥 ∧ 𝜑)) ↔ (𝑧 ∈ 𝑥 ∧ (𝜑 ∧ 𝑡 = 𝑧)))
39	38	exbii 1869	. . . . . . . . . . . . . . . . 17 ⊢ (∃𝑧(𝑧 = 𝑡 ∧ (𝑧 ∈ 𝑥 ∧ 𝜑)) ↔ ∃𝑧(𝑧 ∈ 𝑥 ∧ (𝜑 ∧ 𝑡 = 𝑧)))
40	39	biimpri 230	. . . . . . . . . . . . . . . 16 ⊢ (∃𝑧(𝑧 ∈ 𝑥 ∧ (𝜑 ∧ 𝑡 = 𝑧)) → ∃𝑧(𝑧 = 𝑡 ∧ (𝑧 ∈ 𝑥 ∧ 𝜑)))
41	40	a1i 11	. . . . . . . . . . . . . . 15 ⊢ ([𝑎 / 𝑧](𝑧 ∈ 𝑥 ∧ 𝜑) → (∃𝑧(𝑧 ∈ 𝑥 ∧ (𝜑 ∧ 𝑡 = 𝑧)) → ∃𝑧(𝑧 = 𝑡 ∧ (𝑧 ∈ 𝑥 ∧ 𝜑))))
42		simprr 782	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑧 ∈ 𝑥 ∧ (¬ 𝜑 ∧ 𝑡 = 𝑎)) → 𝑡 = 𝑎)
43	42	exlimiv 1951	. . . . . . . . . . . . . . . 16 ⊢ (∃𝑧(𝑧 ∈ 𝑥 ∧ (¬ 𝜑 ∧ 𝑡 = 𝑎)) → 𝑡 = 𝑎)
44		sbequi 2118	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑎 = 𝑡 → ([𝑎 / 𝑧](𝑧 ∈ 𝑥 ∧ 𝜑) → [𝑡 / 𝑧](𝑧 ∈ 𝑥 ∧ 𝜑)))
45	44	equcoms 2041	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑡 = 𝑎 → ([𝑎 / 𝑧](𝑧 ∈ 𝑥 ∧ 𝜑) → [𝑡 / 𝑧](𝑧 ∈ 𝑥 ∧ 𝜑)))
46	45	com12 32	. . . . . . . . . . . . . . . . 17 ⊢ ([𝑎 / 𝑧](𝑧 ∈ 𝑥 ∧ 𝜑) → (𝑡 = 𝑎 → [𝑡 / 𝑧](𝑧 ∈ 𝑥 ∧ 𝜑)))
47		sb5 2311	. . . . . . . . . . . . . . . . 17 ⊢ ([𝑡 / 𝑧](𝑧 ∈ 𝑥 ∧ 𝜑) ↔ ∃𝑧(𝑧 = 𝑡 ∧ (𝑧 ∈ 𝑥 ∧ 𝜑)))
48	46, 47	imbitrdi 253	. . . . . . . . . . . . . . . 16 ⊢ ([𝑎 / 𝑧](𝑧 ∈ 𝑥 ∧ 𝜑) → (𝑡 = 𝑎 → ∃𝑧(𝑧 = 𝑡 ∧ (𝑧 ∈ 𝑥 ∧ 𝜑))))
49	43, 48	syl5 34	. . . . . . . . . . . . . . 15 ⊢ ([𝑎 / 𝑧](𝑧 ∈ 𝑥 ∧ 𝜑) → (∃𝑧(𝑧 ∈ 𝑥 ∧ (¬ 𝜑 ∧ 𝑡 = 𝑎)) → ∃𝑧(𝑧 = 𝑡 ∧ (𝑧 ∈ 𝑥 ∧ 𝜑))))
50	41, 49	jaod 870	. . . . . . . . . . . . . 14 ⊢ ([𝑎 / 𝑧](𝑧 ∈ 𝑥 ∧ 𝜑) → ((∃𝑧(𝑧 ∈ 𝑥 ∧ (𝜑 ∧ 𝑡 = 𝑧)) ∨ ∃𝑧(𝑧 ∈ 𝑥 ∧ (¬ 𝜑 ∧ 𝑡 = 𝑎))) → ∃𝑧(𝑧 = 𝑡 ∧ (𝑧 ∈ 𝑥 ∧ 𝜑))))
51		orc 878	. . . . . . . . . . . . . . 15 ⊢ (∃𝑧(𝑧 ∈ 𝑥 ∧ (𝜑 ∧ 𝑡 = 𝑧)) → (∃𝑧(𝑧 ∈ 𝑥 ∧ (𝜑 ∧ 𝑡 = 𝑧)) ∨ ∃𝑧(𝑧 ∈ 𝑥 ∧ (¬ 𝜑 ∧ 𝑡 = 𝑎))))
52	39, 51	sylbi 219	. . . . . . . . . . . . . 14 ⊢ (∃𝑧(𝑧 = 𝑡 ∧ (𝑧 ∈ 𝑥 ∧ 𝜑)) → (∃𝑧(𝑧 ∈ 𝑥 ∧ (𝜑 ∧ 𝑡 = 𝑧)) ∨ ∃𝑧(𝑧 ∈ 𝑥 ∧ (¬ 𝜑 ∧ 𝑡 = 𝑎))))
53	50, 52	impbid1 227	. . . . . . . . . . . . 13 ⊢ ([𝑎 / 𝑧](𝑧 ∈ 𝑥 ∧ 𝜑) → ((∃𝑧(𝑧 ∈ 𝑥 ∧ (𝜑 ∧ 𝑡 = 𝑧)) ∨ ∃𝑧(𝑧 ∈ 𝑥 ∧ (¬ 𝜑 ∧ 𝑡 = 𝑎))) ↔ ∃𝑧(𝑧 = 𝑡 ∧ (𝑧 ∈ 𝑥 ∧ 𝜑))))
54	33, 53	bitrid 285	. . . . . . . . . . . 12 ⊢ ([𝑎 / 𝑧](𝑧 ∈ 𝑥 ∧ 𝜑) → (∃𝑧 ∈ 𝑥 ((𝜑 ∧ 𝑡 = 𝑧) ∨ (¬ 𝜑 ∧ 𝑡 = 𝑎)) ↔ ∃𝑧(𝑧 = 𝑡 ∧ (𝑧 ∈ 𝑥 ∧ 𝜑))))
55	54	bibi2d 344	. . . . . . . . . . 11 ⊢ ([𝑎 / 𝑧](𝑧 ∈ 𝑥 ∧ 𝜑) → ((𝑡 ∈ 𝑦 ↔ ∃𝑧 ∈ 𝑥 ((𝜑 ∧ 𝑡 = 𝑧) ∨ (¬ 𝜑 ∧ 𝑡 = 𝑎))) ↔ (𝑡 ∈ 𝑦 ↔ ∃𝑧(𝑧 = 𝑡 ∧ (𝑧 ∈ 𝑥 ∧ 𝜑)))))
56	55	biimpd 231	. . . . . . . . . 10 ⊢ ([𝑎 / 𝑧](𝑧 ∈ 𝑥 ∧ 𝜑) → ((𝑡 ∈ 𝑦 ↔ ∃𝑧 ∈ 𝑥 ((𝜑 ∧ 𝑡 = 𝑧) ∨ (¬ 𝜑 ∧ 𝑡 = 𝑎))) → (𝑡 ∈ 𝑦 ↔ ∃𝑧(𝑧 = 𝑡 ∧ (𝑧 ∈ 𝑥 ∧ 𝜑)))))
57	56	alimdv 1937	. . . . . . . . 9 ⊢ ([𝑎 / 𝑧](𝑧 ∈ 𝑥 ∧ 𝜑) → (∀𝑡(𝑡 ∈ 𝑦 ↔ ∃𝑧 ∈ 𝑥 ((𝜑 ∧ 𝑡 = 𝑧) ∨ (¬ 𝜑 ∧ 𝑡 = 𝑎))) → ∀𝑡(𝑡 ∈ 𝑦 ↔ ∃𝑧(𝑧 = 𝑡 ∧ (𝑧 ∈ 𝑥 ∧ 𝜑)))))
58		nfv 1935	. . . . . . . . . . 11 ⊢ Ⅎ𝑧 𝑡 ∈ 𝑦
59		nfe1 2185	. . . . . . . . . . 11 ⊢ Ⅎ𝑧∃𝑧(𝑧 = 𝑡 ∧ (𝑧 ∈ 𝑥 ∧ 𝜑))
60	58, 59	nfbi 1924	. . . . . . . . . 10 ⊢ Ⅎ𝑧(𝑡 ∈ 𝑦 ↔ ∃𝑧(𝑧 = 𝑡 ∧ (𝑧 ∈ 𝑥 ∧ 𝜑)))
61		nfv 1935	. . . . . . . . . 10 ⊢ Ⅎ𝑡(𝑧 ∈ 𝑦 ↔ (𝑧 ∈ 𝑥 ∧ 𝜑))
62		elequ1 2150	. . . . . . . . . . 11 ⊢ (𝑡 = 𝑧 → (𝑡 ∈ 𝑦 ↔ 𝑧 ∈ 𝑦))
63	47	bicomi 226	. . . . . . . . . . . 12 ⊢ (∃𝑧(𝑧 = 𝑡 ∧ (𝑧 ∈ 𝑥 ∧ 𝜑)) ↔ [𝑡 / 𝑧](𝑧 ∈ 𝑥 ∧ 𝜑))
64		sbequ12r 2288	. . . . . . . . . . . 12 ⊢ (𝑡 = 𝑧 → ([𝑡 / 𝑧](𝑧 ∈ 𝑥 ∧ 𝜑) ↔ (𝑧 ∈ 𝑥 ∧ 𝜑)))
65	63, 64	bitrid 285	. . . . . . . . . . 11 ⊢ (𝑡 = 𝑧 → (∃𝑧(𝑧 = 𝑡 ∧ (𝑧 ∈ 𝑥 ∧ 𝜑)) ↔ (𝑧 ∈ 𝑥 ∧ 𝜑)))
66	62, 65	bibi12d 347	. . . . . . . . . 10 ⊢ (𝑡 = 𝑧 → ((𝑡 ∈ 𝑦 ↔ ∃𝑧(𝑧 = 𝑡 ∧ (𝑧 ∈ 𝑥 ∧ 𝜑))) ↔ (𝑧 ∈ 𝑦 ↔ (𝑧 ∈ 𝑥 ∧ 𝜑))))
67	60, 61, 66	cbvalv1 2373	. . . . . . . . 9 ⊢ (∀𝑡(𝑡 ∈ 𝑦 ↔ ∃𝑧(𝑧 = 𝑡 ∧ (𝑧 ∈ 𝑥 ∧ 𝜑))) ↔ ∀𝑧(𝑧 ∈ 𝑦 ↔ (𝑧 ∈ 𝑥 ∧ 𝜑)))
68	57, 67	imbitrdi 253	. . . . . . . 8 ⊢ ([𝑎 / 𝑧](𝑧 ∈ 𝑥 ∧ 𝜑) → (∀𝑡(𝑡 ∈ 𝑦 ↔ ∃𝑧 ∈ 𝑥 ((𝜑 ∧ 𝑡 = 𝑧) ∨ (¬ 𝜑 ∧ 𝑡 = 𝑎))) → ∀𝑧(𝑧 ∈ 𝑦 ↔ (𝑧 ∈ 𝑥 ∧ 𝜑))))
69	68	eximdv 1938	. . . . . . 7 ⊢ ([𝑎 / 𝑧](𝑧 ∈ 𝑥 ∧ 𝜑) → (∃𝑦∀𝑡(𝑡 ∈ 𝑦 ↔ ∃𝑧 ∈ 𝑥 ((𝜑 ∧ 𝑡 = 𝑧) ∨ (¬ 𝜑 ∧ 𝑡 = 𝑎))) → ∃𝑦∀𝑧(𝑧 ∈ 𝑦 ↔ (𝑧 ∈ 𝑥 ∧ 𝜑))))
70	69	eximi 1856	. . . . . 6 ⊢ (∃𝑎[𝑎 / 𝑧](𝑧 ∈ 𝑥 ∧ 𝜑) → ∃𝑎(∃𝑦∀𝑡(𝑡 ∈ 𝑦 ↔ ∃𝑧 ∈ 𝑥 ((𝜑 ∧ 𝑡 = 𝑧) ∨ (¬ 𝜑 ∧ 𝑡 = 𝑎))) → ∃𝑦∀𝑧(𝑧 ∈ 𝑦 ↔ (𝑧 ∈ 𝑥 ∧ 𝜑))))
71	28, 70	sylbi 219	. . . . 5 ⊢ (∃𝑧 ∈ 𝑥 𝜑 → ∃𝑎(∃𝑦∀𝑡(𝑡 ∈ 𝑦 ↔ ∃𝑧 ∈ 𝑥 ((𝜑 ∧ 𝑡 = 𝑧) ∨ (¬ 𝜑 ∧ 𝑡 = 𝑎))) → ∃𝑦∀𝑧(𝑧 ∈ 𝑦 ↔ (𝑧 ∈ 𝑥 ∧ 𝜑))))
72	71	ax-gen 1816	. . . 4 ⊢ ∀𝑥(∃𝑧 ∈ 𝑥 𝜑 → ∃𝑎(∃𝑦∀𝑡(𝑡 ∈ 𝑦 ↔ ∃𝑧 ∈ 𝑥 ((𝜑 ∧ 𝑡 = 𝑧) ∨ (¬ 𝜑 ∧ 𝑡 = 𝑎))) → ∃𝑦∀𝑧(𝑧 ∈ 𝑦 ↔ (𝑧 ∈ 𝑥 ∧ 𝜑))))
73	24, 72	barbara 2690	. . 3 ⊢ ∀𝑥(∃𝑧 ∈ 𝑥 𝜑 → ∃𝑎∃𝑦∀𝑧(𝑧 ∈ 𝑦 ↔ (𝑧 ∈ 𝑥 ∧ 𝜑)))
74	2, 73	barbara 2690	. 2 ⊢ ∀𝑥(∃𝑧 ∈ 𝑥 𝜑 → ∃𝑦∀𝑧(𝑧 ∈ 𝑦 ↔ (𝑧 ∈ 𝑥 ∧ 𝜑)))
75		ralnex 3089	. . . . 5 ⊢ (∀𝑧 ∈ 𝑥 ¬ 𝜑 ↔ ¬ ∃𝑧 ∈ 𝑥 𝜑)
76		df-ral 3078	. . . . . 6 ⊢ (∀𝑧 ∈ 𝑥 ¬ 𝜑 ↔ ∀𝑧(𝑧 ∈ 𝑥 → ¬ 𝜑))
77		df-ral 3078	. . . . . . 7 ⊢ (∀𝑧 ∈ 𝑦 ⊥ ↔ ∀𝑧(𝑧 ∈ 𝑦 → ⊥))
78		dfnot 1580	. . . . . . . . . . 11 ⊢ (¬ 𝑧 ∈ 𝑦 ↔ (𝑧 ∈ 𝑦 → ⊥))
79	78	bicomi 226	. . . . . . . . . 10 ⊢ ((𝑧 ∈ 𝑦 → ⊥) ↔ ¬ 𝑧 ∈ 𝑦)
80		imnan 403	. . . . . . . . . 10 ⊢ ((𝑧 ∈ 𝑥 → ¬ 𝜑) ↔ ¬ (𝑧 ∈ 𝑥 ∧ 𝜑))
81		pm5.21 834	. . . . . . . . . 10 ⊢ ((¬ 𝑧 ∈ 𝑦 ∧ ¬ (𝑧 ∈ 𝑥 ∧ 𝜑)) → (𝑧 ∈ 𝑦 ↔ (𝑧 ∈ 𝑥 ∧ 𝜑)))
82	79, 80, 81	syl2anb 607	. . . . . . . . 9 ⊢ (((𝑧 ∈ 𝑦 → ⊥) ∧ (𝑧 ∈ 𝑥 → ¬ 𝜑)) → (𝑧 ∈ 𝑦 ↔ (𝑧 ∈ 𝑥 ∧ 𝜑)))
83	82	expcom 417	. . . . . . . 8 ⊢ ((𝑧 ∈ 𝑥 → ¬ 𝜑) → ((𝑧 ∈ 𝑦 → ⊥) → (𝑧 ∈ 𝑦 ↔ (𝑧 ∈ 𝑥 ∧ 𝜑))))
84	83	al2imi 1836	. . . . . . 7 ⊢ (∀𝑧(𝑧 ∈ 𝑥 → ¬ 𝜑) → (∀𝑧(𝑧 ∈ 𝑦 → ⊥) → ∀𝑧(𝑧 ∈ 𝑦 ↔ (𝑧 ∈ 𝑥 ∧ 𝜑))))
85	77, 84	biimtrid 244	. . . . . 6 ⊢ (∀𝑧(𝑧 ∈ 𝑥 → ¬ 𝜑) → (∀𝑧 ∈ 𝑦 ⊥ → ∀𝑧(𝑧 ∈ 𝑦 ↔ (𝑧 ∈ 𝑥 ∧ 𝜑))))
86	76, 85	sylbi 219	. . . . 5 ⊢ (∀𝑧 ∈ 𝑥 ¬ 𝜑 → (∀𝑧 ∈ 𝑦 ⊥ → ∀𝑧(𝑧 ∈ 𝑦 ↔ (𝑧 ∈ 𝑥 ∧ 𝜑))))
87	75, 86	sylbir 237	. . . 4 ⊢ (¬ ∃𝑧 ∈ 𝑥 𝜑 → (∀𝑧 ∈ 𝑦 ⊥ → ∀𝑧(𝑧 ∈ 𝑦 ↔ (𝑧 ∈ 𝑥 ∧ 𝜑))))
88	87	eximdv 1938	. . 3 ⊢ (¬ ∃𝑧 ∈ 𝑥 𝜑 → (∃𝑦∀𝑧 ∈ 𝑦 ⊥ → ∃𝑦∀𝑧(𝑧 ∈ 𝑦 ↔ (𝑧 ∈ 𝑥 ∧ 𝜑))))
89		bj-axseprep.axnulw	. . . 4 ⊢ (∃𝑥⊤ → ∃𝑦∀𝑧 ∈ 𝑦 ⊥)
90		bj-alextruim 37114	. . . 4 ⊢ (∀𝑥∃𝑦∀𝑧 ∈ 𝑦 ⊥ ↔ (∃𝑥⊤ → ∃𝑦∀𝑧 ∈ 𝑦 ⊥))
91	89, 90	mpbir 233	. . 3 ⊢ ∀𝑥∃𝑦∀𝑧 ∈ 𝑦 ⊥
92	88, 91	bj-almpig 37068	. 2 ⊢ ∀𝑥(¬ ∃𝑧 ∈ 𝑥 𝜑 → ∃𝑦∀𝑧(𝑧 ∈ 𝑦 ↔ (𝑧 ∈ 𝑥 ∧ 𝜑)))
93		pm2.61 193	. . 3 ⊢ ((∃𝑧 ∈ 𝑥 𝜑 → ∃𝑦∀𝑧(𝑧 ∈ 𝑦 ↔ (𝑧 ∈ 𝑥 ∧ 𝜑))) → ((¬ ∃𝑧 ∈ 𝑥 𝜑 → ∃𝑦∀𝑧(𝑧 ∈ 𝑦 ↔ (𝑧 ∈ 𝑥 ∧ 𝜑))) → ∃𝑦∀𝑧(𝑧 ∈ 𝑦 ↔ (𝑧 ∈ 𝑥 ∧ 𝜑))))
94	93	al2imi 1836	. 2 ⊢ (∀𝑥(∃𝑧 ∈ 𝑥 𝜑 → ∃𝑦∀𝑧(𝑧 ∈ 𝑦 ↔ (𝑧 ∈ 𝑥 ∧ 𝜑))) → (∀𝑥(¬ ∃𝑧 ∈ 𝑥 𝜑 → ∃𝑦∀𝑧(𝑧 ∈ 𝑦 ↔ (𝑧 ∈ 𝑥 ∧ 𝜑))) → ∀𝑥∃𝑦∀𝑧(𝑧 ∈ 𝑦 ↔ (𝑧 ∈ 𝑥 ∧ 𝜑))))
95	74, 92, 94	mp2 9	1 ⊢ ∀𝑥∃𝑦∀𝑧(𝑧 ∈ 𝑦 ↔ (𝑧 ∈ 𝑥 ∧ 𝜑))

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 208   ∧ wa 399   ∨ wo 858  ∀wal 1559   = wceq 1561  ⊤wtru 1562  ⊥wfal 1573  ∃wex 1800  [wsb 2091   ∈ wcel 2143  ∃!weu 2596  ∀wral 3077  ∃wrex 3087

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1816  ax-4 1830  ax-5 1931  ax-6 1988  ax-7 2029  ax-8 2145  ax-9 2153  ax-10 2176  ax-11 2192  ax-12 2213  ax-ext 2735

This theorem depends on definitions:  df-bi 209  df-an 400  df-or 859  df-tru 1564  df-fal 1574  df-ex 1801  df-nf 1805  df-sb 2092  df-mo 2567  df-eu 2597  df-clab 2742  df-cleq 2755  df-clel 2838  df-ral 3078  df-rex 3088  df-v 3457

This theorem is referenced by: (None)