Metamath Proof Explorer

Theorem sn-axrep5v

Description: A condensed form of axrep5 . (Contributed by SN, 21-Sep-2023)

Ref Expression
Assertion sn-axrep5v ⊢ ∀ w ∈ x ∃* z φ → ∃ y ∀ z z ∈ y ↔ ∃ w ∈ x φ

Proof

Step Hyp Ref Expression
1 axrep6 ⊢ ∀ w ∃* z w ∈ x ∧ φ → ∃ y ∀ z z ∈ y ↔ ∃ w ∈ x w ∈ x ∧ φ
2 19.37v ⊢ ∃ y w ∈ x → ∀ z φ → z = y ↔ w ∈ x → ∃ y ∀ z φ → z = y
3 impexp ⊢ w ∈ x ∧ φ → z = y ↔ w ∈ x → φ → z = y
4 3 albii ⊢ ∀ z w ∈ x ∧ φ → z = y ↔ ∀ z w ∈ x → φ → z = y
5 19.21v ⊢ ∀ z w ∈ x → φ → z = y ↔ w ∈ x → ∀ z φ → z = y
6 4 5 bitri ⊢ ∀ z w ∈ x ∧ φ → z = y ↔ w ∈ x → ∀ z φ → z = y
7 6 exbii ⊢ ∃ y ∀ z w ∈ x ∧ φ → z = y ↔ ∃ y w ∈ x → ∀ z φ → z = y
8 dfmo ⊢ ∃* z φ ↔ ∃ y ∀ z φ → z = y
9 8 imbi2i ⊢ w ∈ x → ∃* z φ ↔ w ∈ x → ∃ y ∀ z φ → z = y
10 2 7 9 3bitr4i ⊢ ∃ y ∀ z w ∈ x ∧ φ → z = y ↔ w ∈ x → ∃* z φ
11 10 albii ⊢ ∀ w ∃ y ∀ z w ∈ x ∧ φ → z = y ↔ ∀ w w ∈ x → ∃* z φ
12 dfmo ⊢ ∃* z w ∈ x ∧ φ ↔ ∃ y ∀ z w ∈ x ∧ φ → z = y
13 12 albii ⊢ ∀ w ∃* z w ∈ x ∧ φ ↔ ∀ w ∃ y ∀ z w ∈ x ∧ φ → z = y
14 df-ral ⊢ ∀ w ∈ x ∃* z φ ↔ ∀ w w ∈ x → ∃* z φ
15 11 13 14 3bitr4i ⊢ ∀ w ∃* z w ∈ x ∧ φ ↔ ∀ w ∈ x ∃* z φ
16 rexanid ⊢ ∃ w ∈ x w ∈ x ∧ φ ↔ ∃ w ∈ x φ
17 16 bibi2i ⊢ z ∈ y ↔ ∃ w ∈ x w ∈ x ∧ φ ↔ z ∈ y ↔ ∃ w ∈ x φ
18 17 albii ⊢ ∀ z z ∈ y ↔ ∃ w ∈ x w ∈ x ∧ φ ↔ ∀ z z ∈ y ↔ ∃ w ∈ x φ
19 18 exbii ⊢ ∃ y ∀ z z ∈ y ↔ ∃ w ∈ x w ∈ x ∧ φ ↔ ∃ y ∀ z z ∈ y ↔ ∃ w ∈ x φ
20 1 15 19 3imtr3i ⊢ ∀ w ∈ x ∃* z φ → ∃ y ∀ z z ∈ y ↔ ∃ w ∈ x φ