Theorem cbvrabv

Description: Rule to change the bound variable in a restricted class abstraction, using implicit substitution. (Contributed by NM, 26-May-1999) Require x , y be disjoint to avoid ax-11 and ax-13 . (Revised by Steven Nguyen, 4-Dec-2022)

	Ref	Expression
Hypothesis	cbvrabv.1	|- ( x = y -> ( ph <-> ps ) )
Assertion	cbvrabv	|- { x e. A | ph } = { y e. A | ps }

Proof

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