Theorem raleqtrdv

Description: Substitution of equal classes into a restricted universal quantifier. (Contributed by Matthew House, 21-Jul-2025)

	Ref	Expression
Hypotheses	raleqtrdv.1	|- ( ph -> A. x e. A ps )
	raleqtrdv.2	|- ( ph -> A = B )
Assertion	raleqtrdv	|- ( ph -> A. x e. B ps )

Proof

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