Metamath Proof Explorer


Theorem hbalw

Description: Weak version of hbal . Uses only Tarski's FOL axiom schemes. Unlike hbal , this theorem requires that x and y be distinct, i.e., not be bundled. (Contributed by NM, 19-Apr-2017)

Ref Expression
Hypotheses hbalw.1 x = z φ ψ
hbalw.2 φ x φ
Assertion hbalw y φ x y φ

Proof

Step Hyp Ref Expression
1 hbalw.1 x = z φ ψ
2 hbalw.2 φ x φ
3 2 alimi y φ y x φ
4 1 alcomiw y x φ x y φ
5 3 4 syl y φ x y φ