Theorem rabeqbii

Description: Equality theorem for restricted class abstractions. Inference version. (Contributed by GG, 1-Sep-2025)

	Ref	Expression
Hypotheses	rabeqbii.1	|- A = B
	rabeqbii.2	|- ( ph <-> ps )
Assertion	rabeqbii	|- { x e. A | ph } = { x e. B | ps }

Proof

Step	Hyp	Ref	Expression
1		rabeqbii.1	|- A = B
2		rabeqbii.2	|- ( ph <-> ps )
3	1	eleq2i	|- ( x e. A <-> x e. B )
4	3 2	anbi12i	|- ( ( x e. A /\ ph ) <-> ( x e. B /\ ps ) )
5	4	abbii	|- { x | ( x e. A /\ ph ) } = { x | ( x e. B /\ ps ) }
6		df-rab	|- { x e. A | ph } = { x | ( x e. A /\ ph ) }
7		df-rab	|- { x e. B | ps } = { x | ( x e. B /\ ps ) }
8	5 6 7	3eqtr4i	|- { x e. A | ph } = { x e. B | ps }