Theorem raleqdv

Description: Equality deduction for restricted universal quantifier. (Contributed by NM, 13-Nov-2005)

	Ref	Expression
Hypothesis	raleqdv.1	|- ( ph -> A = B )
Assertion	raleqdv	|- ( ph -> ( A. x e. A ps <-> A. x e. B ps ) )

Proof

Step	Hyp	Ref	Expression
1		raleqdv.1	|- ( ph -> A = B )
2		raleq	|- ( A = B -> ( A. x e. A ps <-> A. x e. B ps ) )
3	1 2	syl	|- ( ph -> ( A. x e. A ps <-> A. x e. B ps ) )