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 )