Theorem raleqd

Description: Equality deduction for restricted universal quantifier. (Contributed by Glauco Siliprandi, 23-Oct-2021)

	Ref	Expression
Hypotheses	raleqd.a	|- F/_ x A
	raleqd.b	|- F/_ x B
	raleqd.e	|- ( ph -> A = B )
Assertion	raleqd	|- ( ph -> ( A. x e. A ps <-> A. x e. B ps ) )

Proof

Step	Hyp	Ref	Expression
1		raleqd.a	|- F/_ x A
2		raleqd.b	|- F/_ x B
3		raleqd.e	|- ( ph -> A = B )
4	1 2	raleqf	|- ( A = B -> ( A. x e. A ps <-> A. x e. B ps ) )
5	3 4	syl	|- ( ph -> ( A. x e. A ps <-> A. x e. B ps ) )