Theorem raleqbi1dv

Description: Equality deduction for restricted universal quantifier. (Contributed by NM, 16-Nov-1995) (Proof shortened by Steven Nguyen, 5-May-2023)

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

Proof

Step	Hyp	Ref	Expression
1		raleqbi1dv.1	|- ( A = B -> ( ph <-> ps ) )
2		id	|- ( A = B -> A = B )
3	2 1	raleqbidvv	|- ( A = B -> ( A. x e. A ph <-> A. x e. B ps ) )