Metamath Proof Explorer

Theorem bj-axseprep

Description: Axiom of separation (universal closure of ax-sep ) 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 ) 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 and sbequ12r and eueq2 ) could be reworked to avoid it. Proof modifications should not introduce steps relying on a nonempty universe, like alrimiv . (Contributed by BJ, 14-Mar-2026) (Proof modification is discouraged.)

Ref Expression
Hypotheses bj-axseprep.axnulw ⊢ ∃ x ⊤ → ∃ y ∀ z ∈ y ⊥
bj-axseprep.axrep ⊢ ∀ x ∀ z ∈ x ∃! t ψ → ∃ y ∀ t t ∈ y ↔ ∃ z ∈ x ψ
bj-axseprep.ps ⊢ ψ ↔ φ ∧ t = z ∨ ¬ φ ∧ t = a
Assertion bj-axseprep ⊢ ∀ x ∃ y ∀ z z ∈ y ↔ z ∈ x ∧ φ

Proof

Step Hyp Ref Expression
1 bj-axseprep.axnulw ⊢ ∃ x ⊤ → ∃ y ∀ z ∈ y ⊥
2 bj-axseprep.axrep ⊢ ∀ x ∀ z ∈ x ∃! t ψ → ∃ y ∀ t t ∈ y ↔ ∃ z ∈ x ψ
3 bj-axseprep.ps ⊢ ψ ↔ φ ∧ t = z ∨ ¬ φ ∧ t = a
4 ax5e ⊢ ∃ a ∃ y ∀ z z ∈ y ↔ z ∈ x ∧ φ → ∃ y ∀ z z ∈ y ↔ z ∈ x ∧ φ
5 4 ax-gen ⊢ ∀ x ∃ a ∃ y ∀ z z ∈ y ↔ z ∈ x ∧ φ → ∃ y ∀ z z ∈ y ↔ z ∈ x ∧ φ
6 bj-eximcom ⊢ ∃ a ∃ y ∀ t t ∈ y ↔ ∃ z ∈ x φ ∧ t = z ∨ ¬ φ ∧ t = a → ∃ y ∀ z z ∈ y ↔ z ∈ x ∧ φ → ∀ a ∃ y ∀ t t ∈ y ↔ ∃ z ∈ x φ ∧ t = z ∨ ¬ φ ∧ t = a → ∃ a ∃ y ∀ z z ∈ y ↔ z ∈ x ∧ φ
7 3 eubii ⊢ ∃! t ψ ↔ ∃! t φ ∧ t = z ∨ ¬ φ ∧ t = a
8 7 ralbii ⊢ ∀ z ∈ x ∃! t ψ ↔ ∀ z ∈ x ∃! t φ ∧ t = z ∨ ¬ φ ∧ t = a
9 3 rexbii ⊢ ∃ z ∈ x ψ ↔ ∃ z ∈ x φ ∧ t = z ∨ ¬ φ ∧ t = a
10 9 bibi2i ⊢ t ∈ y ↔ ∃ z ∈ x ψ ↔ t ∈ y ↔ ∃ z ∈ x φ ∧ t = z ∨ ¬ φ ∧ t = a
11 10 albii ⊢ ∀ t t ∈ y ↔ ∃ z ∈ x ψ ↔ ∀ t t ∈ y ↔ ∃ z ∈ x φ ∧ t = z ∨ ¬ φ ∧ t = a
12 11 exbii ⊢ ∃ y ∀ t t ∈ y ↔ ∃ z ∈ x ψ ↔ ∃ y ∀ t t ∈ y ↔ ∃ z ∈ x φ ∧ t = z ∨ ¬ φ ∧ t = a
13 8 12 imbi12i ⊢ ∀ z ∈ x ∃! t ψ → ∃ y ∀ t t ∈ y ↔ ∃ z ∈ x ψ ↔ ∀ z ∈ x ∃! t φ ∧ t = z ∨ ¬ φ ∧ t = a → ∃ y ∀ t t ∈ y ↔ ∃ z ∈ x φ ∧ t = z ∨ ¬ φ ∧ t = a
14 13 albii ⊢ ∀ x ∀ z ∈ x ∃! t ψ → ∃ y ∀ t t ∈ y ↔ ∃ z ∈ x ψ ↔ ∀ x ∀ z ∈ x ∃! t φ ∧ t = z ∨ ¬ φ ∧ t = a → ∃ y ∀ t t ∈ y ↔ ∃ z ∈ x φ ∧ t = z ∨ ¬ φ ∧ t = a
15 2 14 mpbi ⊢ ∀ x ∀ z ∈ x ∃! t φ ∧ t = z ∨ ¬ φ ∧ t = a → ∃ y ∀ t t ∈ y ↔ ∃ z ∈ x φ ∧ t = z ∨ ¬ φ ∧ t = a
16 vex ⊢ z ∈ V
17 vex ⊢ a ∈ V
18 16 17 eueq2 ⊢ ∃! t φ ∧ t = z ∨ ¬ φ ∧ t = a
19 18 rgenw ⊢ ∀ z ∈ x ∃! t φ ∧ t = z ∨ ¬ φ ∧ t = a
20 19 ax-gen ⊢ ∀ x ∀ z ∈ x ∃! t φ ∧ t = z ∨ ¬ φ ∧ t = a
21 15 20 bj-almp ⊢ ∀ x ∃ y ∀ t t ∈ y ↔ ∃ z ∈ x φ ∧ t = z ∨ ¬ φ ∧ t = a
22 21 ax-gen ⊢ ∀ a ∀ x ∃ y ∀ t t ∈ y ↔ ∃ z ∈ x φ ∧ t = z ∨ ¬ φ ∧ t = a
23 alcom ⊢ ∀ a ∀ x ∃ y ∀ t t ∈ y ↔ ∃ z ∈ x φ ∧ t = z ∨ ¬ φ ∧ t = a ↔ ∀ x ∀ a ∃ y ∀ t t ∈ y ↔ ∃ z ∈ x φ ∧ t = z ∨ ¬ φ ∧ t = a
24 22 23 mpbi ⊢ ∀ x ∀ a ∃ y ∀ t t ∈ y ↔ ∃ z ∈ x φ ∧ t = z ∨ ¬ φ ∧ t = a
25 6 24 bj-almpig ⊢ ∀ x ∃ a ∃ y ∀ t t ∈ y ↔ ∃ z ∈ x φ ∧ t = z ∨ ¬ φ ∧ t = a → ∃ y ∀ z z ∈ y ↔ z ∈ x ∧ φ → ∃ a ∃ y ∀ z z ∈ y ↔ z ∈ x ∧ φ
26 df-rex ⊢ ∃ z ∈ x φ ↔ ∃ z z ∈ x ∧ φ
27 nfv ⊢ Ⅎ a z ∈ x ∧ φ
28 27 sb8ef ⊢ ∃ z z ∈ x ∧ φ ↔ ∃ a a z z ∈ x ∧ φ
29 26 28 bitri ⊢ ∃ z ∈ x φ ↔ ∃ a a z z ∈ x ∧ φ
30 df-rex ⊢ ∃ z ∈ x φ ∧ t = z ∨ ¬ φ ∧ t = a ↔ ∃ z z ∈ x ∧ φ ∧ t = z ∨ ¬ φ ∧ t = a
31 andi ⊢ z ∈ x ∧ φ ∧ t = z ∨ ¬ φ ∧ t = a ↔ z ∈ x ∧ φ ∧ t = z ∨ z ∈ x ∧ ¬ φ ∧ t = a
32 31 exbii ⊢ ∃ z z ∈ x ∧ φ ∧ t = z ∨ ¬ φ ∧ t = a ↔ ∃ z z ∈ x ∧ φ ∧ t = z ∨ z ∈ x ∧ ¬ φ ∧ t = a
33 19.43 ⊢ ∃ z z ∈ x ∧ φ ∧ t = z ∨ z ∈ x ∧ ¬ φ ∧ t = a ↔ ∃ z z ∈ x ∧ φ ∧ t = z ∨ ∃ z z ∈ x ∧ ¬ φ ∧ t = a
34 30 32 33 3bitri ⊢ ∃ z ∈ x φ ∧ t = z ∨ ¬ φ ∧ t = a ↔ ∃ z z ∈ x ∧ φ ∧ t = z ∨ ∃ z z ∈ x ∧ ¬ φ ∧ t = a
35 equcom ⊢ z = t ↔ t = z
36 35 anbi1i ⊢ z = t ∧ z ∈ x ∧ φ ↔ t = z ∧ z ∈ x ∧ φ
37 ancom ⊢ t = z ∧ z ∈ x ∧ φ ↔ z ∈ x ∧ φ ∧ t = z
38 anass ⊢ z ∈ x ∧ φ ∧ t = z ↔ z ∈ x ∧ φ ∧ t = z
39 36 37 38 3bitri ⊢ z = t ∧ z ∈ x ∧ φ ↔ z ∈ x ∧ φ ∧ t = z
40 39 exbii ⊢ ∃ z z = t ∧ z ∈ x ∧ φ ↔ ∃ z z ∈ x ∧ φ ∧ t = z
41 40 biimpri ⊢ ∃ z z ∈ x ∧ φ ∧ t = z → ∃ z z = t ∧ z ∈ x ∧ φ
42 41 a1i ⊢ a z z ∈ x ∧ φ → ∃ z z ∈ x ∧ φ ∧ t = z → ∃ z z = t ∧ z ∈ x ∧ φ
43 simprr ⊢ z ∈ x ∧ ¬ φ ∧ t = a → t = a
44 43 exlimiv ⊢ ∃ z z ∈ x ∧ ¬ φ ∧ t = a → t = a
45 sbequi ⊢ a = t → a z z ∈ x ∧ φ → t z z ∈ x ∧ φ
46 45 equcoms ⊢ t = a → a z z ∈ x ∧ φ → t z z ∈ x ∧ φ
47 46 com12 ⊢ a z z ∈ x ∧ φ → t = a → t z z ∈ x ∧ φ
48 sb5 ⊢ t z z ∈ x ∧ φ ↔ ∃ z z = t ∧ z ∈ x ∧ φ
49 47 48 imbitrdi ⊢ a z z ∈ x ∧ φ → t = a → ∃ z z = t ∧ z ∈ x ∧ φ
50 44 49 syl5 ⊢ a z z ∈ x ∧ φ → ∃ z z ∈ x ∧ ¬ φ ∧ t = a → ∃ z z = t ∧ z ∈ x ∧ φ
51 42 50 jaod ⊢ a z z ∈ x ∧ φ → ∃ z z ∈ x ∧ φ ∧ t = z ∨ ∃ z z ∈ x ∧ ¬ φ ∧ t = a → ∃ z z = t ∧ z ∈ x ∧ φ
52 orc ⊢ ∃ z z ∈ x ∧ φ ∧ t = z → ∃ z z ∈ x ∧ φ ∧ t = z ∨ ∃ z z ∈ x ∧ ¬ φ ∧ t = a
53 40 52 sylbi ⊢ ∃ z z = t ∧ z ∈ x ∧ φ → ∃ z z ∈ x ∧ φ ∧ t = z ∨ ∃ z z ∈ x ∧ ¬ φ ∧ t = a
54 51 53 impbid1 ⊢ a z z ∈ x ∧ φ → ∃ z z ∈ x ∧ φ ∧ t = z ∨ ∃ z z ∈ x ∧ ¬ φ ∧ t = a ↔ ∃ z z = t ∧ z ∈ x ∧ φ
55 34 54 bitrid ⊢ a z z ∈ x ∧ φ → ∃ z ∈ x φ ∧ t = z ∨ ¬ φ ∧ t = a ↔ ∃ z z = t ∧ z ∈ x ∧ φ
56 55 bibi2d ⊢ a z z ∈ x ∧ φ → t ∈ y ↔ ∃ z ∈ x φ ∧ t = z ∨ ¬ φ ∧ t = a ↔ t ∈ y ↔ ∃ z z = t ∧ z ∈ x ∧ φ
57 56 biimpd ⊢ a z z ∈ x ∧ φ → t ∈ y ↔ ∃ z ∈ x φ ∧ t = z ∨ ¬ φ ∧ t = a → t ∈ y ↔ ∃ z z = t ∧ z ∈ x ∧ φ
58 57 alimdv ⊢ a z z ∈ x ∧ φ → ∀ t t ∈ y ↔ ∃ z ∈ x φ ∧ t = z ∨ ¬ φ ∧ t = a → ∀ t t ∈ y ↔ ∃ z z = t ∧ z ∈ x ∧ φ
59 nfv ⊢ Ⅎ z t ∈ y
60 nfe1 ⊢ Ⅎ z ∃ z z = t ∧ z ∈ x ∧ φ
61 59 60 nfbi ⊢ Ⅎ z t ∈ y ↔ ∃ z z = t ∧ z ∈ x ∧ φ
62 nfv ⊢ Ⅎ t z ∈ y ↔ z ∈ x ∧ φ
63 elequ1 ⊢ t = z → t ∈ y ↔ z ∈ y
64 48 bicomi ⊢ ∃ z z = t ∧ z ∈ x ∧ φ ↔ t z z ∈ x ∧ φ
65 sbequ12r ⊢ t = z → t z z ∈ x ∧ φ ↔ z ∈ x ∧ φ
66 64 65 bitrid ⊢ t = z → ∃ z z = t ∧ z ∈ x ∧ φ ↔ z ∈ x ∧ φ
67 63 66 bibi12d ⊢ t = z → t ∈ y ↔ ∃ z z = t ∧ z ∈ x ∧ φ ↔ z ∈ y ↔ z ∈ x ∧ φ
68 61 62 67 cbvalv1 ⊢ ∀ t t ∈ y ↔ ∃ z z = t ∧ z ∈ x ∧ φ ↔ ∀ z z ∈ y ↔ z ∈ x ∧ φ
69 58 68 imbitrdi ⊢ a z z ∈ x ∧ φ → ∀ t t ∈ y ↔ ∃ z ∈ x φ ∧ t = z ∨ ¬ φ ∧ t = a → ∀ z z ∈ y ↔ z ∈ x ∧ φ
70 69 eximdv ⊢ a z z ∈ x ∧ φ → ∃ y ∀ t t ∈ y ↔ ∃ z ∈ x φ ∧ t = z ∨ ¬ φ ∧ t = a → ∃ y ∀ z z ∈ y ↔ z ∈ x ∧ φ
71 70 eximi ⊢ ∃ a a z z ∈ x ∧ φ → ∃ a ∃ y ∀ t t ∈ y ↔ ∃ z ∈ x φ ∧ t = z ∨ ¬ φ ∧ t = a → ∃ y ∀ z z ∈ y ↔ z ∈ x ∧ φ
72 29 71 sylbi ⊢ ∃ z ∈ x φ → ∃ a ∃ y ∀ t t ∈ y ↔ ∃ z ∈ x φ ∧ t = z ∨ ¬ φ ∧ t = a → ∃ y ∀ z z ∈ y ↔ z ∈ x ∧ φ
73 72 ax-gen ⊢ ∀ x ∃ z ∈ x φ → ∃ a ∃ y ∀ t t ∈ y ↔ ∃ z ∈ x φ ∧ t = z ∨ ¬ φ ∧ t = a → ∃ y ∀ z z ∈ y ↔ z ∈ x ∧ φ
74 25 73 barbara ⊢ ∀ x ∃ z ∈ x φ → ∃ a ∃ y ∀ z z ∈ y ↔ z ∈ x ∧ φ
75 5 74 barbara ⊢ ∀ x ∃ z ∈ x φ → ∃ y ∀ z z ∈ y ↔ z ∈ x ∧ φ
76 ralnex ⊢ ∀ z ∈ x ¬ φ ↔ ¬ ∃ z ∈ x φ
77 df-ral ⊢ ∀ z ∈ x ¬ φ ↔ ∀ z z ∈ x → ¬ φ
78 df-ral ⊢ ∀ z ∈ y ⊥ ↔ ∀ z z ∈ y → ⊥
79 dfnot ⊢ ¬ z ∈ y ↔ z ∈ y → ⊥
80 79 bicomi ⊢ z ∈ y → ⊥ ↔ ¬ z ∈ y
81 imnan ⊢ z ∈ x → ¬ φ ↔ ¬ z ∈ x ∧ φ
82 pm5.21 ⊢ ¬ z ∈ y ∧ ¬ z ∈ x ∧ φ → z ∈ y ↔ z ∈ x ∧ φ
83 80 81 82 syl2anb ⊢ z ∈ y → ⊥ ∧ z ∈ x → ¬ φ → z ∈ y ↔ z ∈ x ∧ φ
84 83 expcom ⊢ z ∈ x → ¬ φ → z ∈ y → ⊥ → z ∈ y ↔ z ∈ x ∧ φ
85 84 al2imi ⊢ ∀ z z ∈ x → ¬ φ → ∀ z z ∈ y → ⊥ → ∀ z z ∈ y ↔ z ∈ x ∧ φ
86 78 85 biimtrid ⊢ ∀ z z ∈ x → ¬ φ → ∀ z ∈ y ⊥ → ∀ z z ∈ y ↔ z ∈ x ∧ φ
87 77 86 sylbi ⊢ ∀ z ∈ x ¬ φ → ∀ z ∈ y ⊥ → ∀ z z ∈ y ↔ z ∈ x ∧ φ
88 76 87 sylbir ⊢ ¬ ∃ z ∈ x φ → ∀ z ∈ y ⊥ → ∀ z z ∈ y ↔ z ∈ x ∧ φ
89 88 eximdv ⊢ ¬ ∃ z ∈ x φ → ∃ y ∀ z ∈ y ⊥ → ∃ y ∀ z z ∈ y ↔ z ∈ x ∧ φ
90 bj-alextruim ⊢ ∀ x ∃ y ∀ z ∈ y ⊥ ↔ ∃ x ⊤ → ∃ y ∀ z ∈ y ⊥
91 1 90 mpbir ⊢ ∀ x ∃ y ∀ z ∈ y ⊥
92 89 91 bj-almpig ⊢ ∀ x ¬ ∃ z ∈ x φ → ∃ y ∀ z z ∈ y ↔ z ∈ x ∧ φ
93 pm2.61 ⊢ ∃ z ∈ x φ → ∃ y ∀ z z ∈ y ↔ z ∈ x ∧ φ → ¬ ∃ z ∈ x φ → ∃ y ∀ z z ∈ y ↔ z ∈ x ∧ φ → ∃ y ∀ z z ∈ y ↔ z ∈ x ∧ φ
94 93 al2imi ⊢ ∀ x ∃ z ∈ x φ → ∃ y ∀ z z ∈ y ↔ z ∈ x ∧ φ → ∀ x ¬ ∃ z ∈ x φ → ∃ y ∀ z z ∈ y ↔ z ∈ x ∧ φ → ∀ x ∃ y ∀ z z ∈ y ↔ z ∈ x ∧ φ
95 75 92 94 mp2 ⊢ ∀ x ∃ y ∀ z z ∈ y ↔ z ∈ x ∧ φ