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