Metamath Proof Explorer


Theorem bj-equsexval

Description: Special case of equsexv proved from core axioms, ax-10 (modal5), and hba1 (modal4). (Contributed by BJ, 29-Dec-2020) (Proof modification is discouraged.)

Ref Expression
Hypothesis bj-equsexval.1 x = y φ x ψ
Assertion bj-equsexval x x = y φ x ψ

Proof

Step Hyp Ref Expression
1 bj-equsexval.1 x = y φ x ψ
2 1 pm5.32i x = y φ x = y x ψ
3 2 exbii x x = y φ x x = y x ψ
4 ax6ev x x = y
5 bj-19.41al x x = y x ψ x x = y x ψ
6 4 5 mpbiran x x = y x ψ x ψ
7 3 6 bitri x x = y φ x ψ