Theorem cbvrabv2w

Description: A more general version of cbvrabv . Version of cbvrabv2 with a disjoint variable condition, which does not require ax-13 . (Contributed by Glauco Siliprandi, 23-Oct-2021) (Revised by GG, 14-Aug-2025)

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

Proof

Step	Hyp	Ref	Expression
1		cbvrabv2w.1	|- ( x = y -> A = B )
2		cbvrabv2w.2	|- ( x = y -> ( ph <-> ps ) )
3		id	|- ( x = y -> x = y )
4	3 1	eleq12d	|- ( x = y -> ( x e. A <-> y e. B ) )
5	4 2	anbi12d	|- ( x = y -> ( ( x e. A /\ ph ) <-> ( y e. B /\ ps ) ) )
6	5	cbvabv	|- { x | ( x e. A /\ ph ) } = { y | ( y e. B /\ ps ) }
7		df-rab	|- { x e. A | ph } = { x | ( x e. A /\ ph ) }
8		df-rab	|- { y e. B | ps } = { y | ( y e. B /\ ps ) }
9	6 7 8	3eqtr4i	|- { x e. A | ph } = { y e. B | ps }