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

Metamath Proof Explorer

Theorem hbsbwOLD

Description: Obsolete version of hbsbw as of 14-May-2025. (Contributed by NM, 12-Aug-1993) (Revised by GG, 23-May-2024) (New usage is discouraged.) (Proof modification is discouraged.)

Ref Expression
Hypothesis hbsbw.1 ⊢ φ → ∀ z φ
Assertion hbsbwOLD ⊢ y x φ → ∀ z y x φ

Proof

Step Hyp Ref Expression
1 hbsbw.1 ⊢ φ → ∀ z φ
2 dfsb ⊢ y x φ ↔ ∀ w w = y → ∀ x x = w → φ
3 1 imim2i ⊢ x = w → φ → x = w → ∀ z φ
4 3 alimi ⊢ ∀ x x = w → φ → ∀ x x = w → ∀ z φ
5 19.21v ⊢ ∀ z x = w → φ ↔ x = w → ∀ z φ
6 5 biimpri ⊢ x = w → ∀ z φ → ∀ z x = w → φ
7 6 alimi ⊢ ∀ x x = w → ∀ z φ → ∀ x ∀ z x = w → φ
8 ax-11 ⊢ ∀ x ∀ z x = w → φ → ∀ z ∀ x x = w → φ
9 4 7 8 3syl ⊢ ∀ x x = w → φ → ∀ z ∀ x x = w → φ
10 9 imim2i ⊢ w = y → ∀ x x = w → φ → w = y → ∀ z ∀ x x = w → φ
11 19.21v ⊢ ∀ z w = y → ∀ x x = w → φ ↔ w = y → ∀ z ∀ x x = w → φ
12 10 11 sylibr ⊢ w = y → ∀ x x = w → φ → ∀ z w = y → ∀ x x = w → φ
13 12 hbal ⊢ ∀ w w = y → ∀ x x = w → φ → ∀ z ∀ w w = y → ∀ x x = w → φ
14 2 13 hbxfrbi ⊢ y x φ → ∀ z y x φ