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, 31May2019)
Ref  Expression  

Hypothesis  equsalvw.1   ( x = y > ( ph <> ps ) ) 

Assertion  equsalvw   ( A. x ( x = y > ph ) <> ps ) 
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 ) 