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

Metamath Proof Explorer

Theorem bj-hbsb2av

Description: Version of hbsb2a with a disjoint variable condition, which does not require ax-13 . (Contributed by BJ, 11-Sep-2019) (Proof modification is discouraged.)

Ref Expression
Assertion bj-hbsb2av ⊢ y x ∀ y φ → ∀ x y x φ

Proof

Step Hyp Ref Expression
1 sb4av ⊢ y x ∀ y φ → ∀ x x = y → φ
2 sb6 ⊢ y x φ ↔ ∀ x x = y → φ
3 2 biimpri ⊢ ∀ x x = y → φ → y x φ
4 3 axc4i ⊢ ∀ x x = y → φ → ∀ x y x φ
5 1 4 syl ⊢ y x ∀ y φ → ∀ x y x φ