Theorem equsalh

Description: An equivalence related to implicit substitution. Usage of this theorem is discouraged because it depends on ax-13 . See equsalhw for a version with a disjoint variable condition requiring fewer axioms. (Contributed by NM, 2-Jun-1993) (New usage is discouraged.)

	Ref	Expression
Hypotheses	equsalh.1	|- ( ps -> A. x ps )
	equsalh.2	|- ( x = y -> ( ph <-> ps ) )
Assertion	equsalh	|- ( A. x ( x = y -> ph ) <-> ps )

Proof

Step	Hyp	Ref	Expression
1		equsalh.1	|- ( ps -> A. x ps )
2		equsalh.2	|- ( x = y -> ( ph <-> ps ) )
3	1	nf5i	|- F/ x ps
4	3 2	equsal	|- ( A. x ( x = y -> ph ) <-> ps )