Metamath Proof Explorer


Theorem equsalvw

Description: Version of equsalv with a disjoint variable condition, and of equsal with two disjoint variable conditions, which requires fewer axioms. See also the dual form equsexvw . (Contributed by BJ, 31-May-2019)

Ref Expression
Hypothesis equsalvw.1
|- ( x = y -> ( ph <-> ps ) )
Assertion equsalvw
|- ( A. x ( x = y -> ph ) <-> ps )

Proof

Step Hyp Ref Expression
1 equsalvw.1
 |-  ( x = y -> ( ph <-> ps ) )
2 1 pm5.74i
 |-  ( ( x = y -> ph ) <-> ( x = y -> ps ) )
3 2 albii
 |-  ( A. x ( x = y -> ph ) <-> A. x ( x = y -> ps ) )
4 equsv
 |-  ( A. x ( x = y -> ps ) <-> ps )
5 3 4 bitri
 |-  ( A. x ( x = y -> ph ) <-> ps )