Metamath Proof Explorer

Theorem axrep6

Description: A condensed form of ax-rep . (Contributed by SN, 18-Sep-2023)

Ref Expression
Assertion axrep6 ⊢ ∀ 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 φ