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

Metamath Proof Explorer

Theorem axrep4v

Description: Version of axrep4 with a disjoint variable condition, requiring fewer axioms. (Contributed by Matthew House, 18-Sep-2025)

Ref Expression
Assertion axrep4v ⊢ ∀ x ∃ z ∀ y φ → y = z → ∃ z ∀ y y ∈ z ↔ ∃ x x ∈ w ∧ φ

Proof

Step Hyp Ref Expression
1 ax-rep ⊢ ∀ x ∃ z ∀ y ∀ z φ → y = z → ∃ z ∀ y y ∈ z ↔ ∃ x x ∈ w ∧ ∀ z φ
2 19.3v ⊢ ∀ z φ ↔ φ
3 2 imbi1i ⊢ ∀ z φ → y = z ↔ φ → y = z
4 3 albii ⊢ ∀ y ∀ z φ → y = z ↔ ∀ y φ → y = z
5 4 exbii ⊢ ∃ z ∀ y ∀ z φ → y = z ↔ ∃ z ∀ y φ → y = z
6 5 albii ⊢ ∀ x ∃ z ∀ y ∀ z φ → y = z ↔ ∀ x ∃ z ∀ y φ → y = z
7 2 anbi2i ⊢ x ∈ w ∧ ∀ z φ ↔ x ∈ w ∧ φ
8 7 exbii ⊢ ∃ x x ∈ w ∧ ∀ z φ ↔ ∃ x x ∈ w ∧ φ
9 8 bibi2i ⊢ y ∈ z ↔ ∃ x x ∈ w ∧ ∀ z φ ↔ y ∈ z ↔ ∃ x x ∈ w ∧ φ
10 9 albii ⊢ ∀ y y ∈ z ↔ ∃ x x ∈ w ∧ ∀ z φ ↔ ∀ y y ∈ z ↔ ∃ x x ∈ w ∧ φ
11 10 exbii ⊢ ∃ z ∀ y y ∈ z ↔ ∃ x x ∈ w ∧ ∀ z φ ↔ ∃ z ∀ y y ∈ z ↔ ∃ x x ∈ w ∧ φ
12 1 6 11 3imtr3i ⊢ ∀ x ∃ z ∀ y φ → y = z → ∃ z ∀ y y ∈ z ↔ ∃ x x ∈ w ∧ φ