This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem axrep6OLD

Description: Obsolete version of axrep6 as of 18-Sep-2025. (Contributed by SN, 18-Sep-2023) (Proof modification is discouraged.) (New usage is discouraged.)

Ref Expression
Assertion axrep6OLD ⊢ ∀ w ∃* z φ → ∃ y ∀ z z ∈ y ↔ ∃ w ∈ x φ

Proof

Step Hyp Ref Expression
1 ax-rep ⊢ ∀ w ∃ y ∀ z ∀ y φ → z = y → ∃ y ∀ z z ∈ y ↔ ∃ w w ∈ x ∧ ∀ y φ
2 df-mo ⊢ ∃* z φ ↔ ∃ y ∀ z φ → z = y
3 19.3v ⊢ ∀ y φ ↔ φ
4 3 imbi1i ⊢ ∀ y φ → z = y ↔ φ → z = y
5 4 albii ⊢ ∀ z ∀ y φ → z = y ↔ ∀ z φ → z = y
6 5 exbii ⊢ ∃ y ∀ z ∀ y φ → z = y ↔ ∃ y ∀ z φ → z = y
7 2 6 bitr4i ⊢ ∃* z φ ↔ ∃ y ∀ z ∀ y φ → z = y
8 7 albii ⊢ ∀ w ∃* z φ ↔ ∀ w ∃ y ∀ z ∀ y φ → z = y
9 3 rexbii ⊢ ∃ w ∈ x ∀ y φ ↔ ∃ w ∈ x φ
10 df-rex ⊢ ∃ w ∈ x ∀ y φ ↔ ∃ w w ∈ x ∧ ∀ y φ
11 9 10 bitr3i ⊢ ∃ w ∈ x φ ↔ ∃ w w ∈ x ∧ ∀ y φ
12 11 bibi2i ⊢ z ∈ y ↔ ∃ w ∈ x φ ↔ z ∈ y ↔ ∃ w w ∈ x ∧ ∀ y φ
13 12 albii ⊢ ∀ z z ∈ y ↔ ∃ w ∈ x φ ↔ ∀ z z ∈ y ↔ ∃ w w ∈ x ∧ ∀ y φ
14 13 exbii ⊢ ∃ y ∀ z z ∈ y ↔ ∃ w ∈ x φ ↔ ∃ y ∀ z z ∈ y ↔ ∃ w w ∈ x ∧ ∀ y φ
15 1 8 14 3imtr4i ⊢ ∀ w ∃* z φ → ∃ y ∀ z z ∈ y ↔ ∃ w ∈ x φ