Theorem cbvrabw

Description: Rule to change the bound variable in a restricted class abstraction, using implicit substitution. Version of cbvrab with a disjoint variable condition, which does not require ax-13 . (Contributed by Andrew Salmon, 11-Jul-2011) Avoid ax-13 . (Revised by GG, 10-Jan-2024) Avoid ax-10 . (Revised by Wolf Lammen, 19-Jul-2025)

	Ref	Expression
Hypotheses	cbvrabw.1	|- F/_ x A
	cbvrabw.2	|- F/_ y A
	cbvrabw.3	|- F/ y ph
	cbvrabw.4	|- F/ x ps
	cbvrabw.5	|- ( x = y -> ( ph <-> ps ) )
Assertion	cbvrabw	|- { x e. A | ph } = { y e. A | ps }

Proof

Step	Hyp	Ref	Expression
1		cbvrabw.1	|- F/_ x A
2		cbvrabw.2	|- F/_ y A
3		cbvrabw.3	|- F/ y ph
4		cbvrabw.4	|- F/ x ps
5		cbvrabw.5	|- ( x = y -> ( ph <-> ps ) )
6	2	nfcri	|- F/ y x e. A
7	6 3	nfan	|- F/ y ( x e. A /\ ph )
8	1	nfcri	|- F/ x y e. A
9	8 4	nfan	|- F/ x ( y e. A /\ ps )
10		eleq1w	|- ( x = y -> ( x e. A <-> y e. A ) )
11	10 5	anbi12d	|- ( x = y -> ( ( x e. A /\ ph ) <-> ( y e. A /\ ps ) ) )
12	7 9 11	cbvabw	|- { x | ( x e. A /\ ph ) } = { y | ( y e. A /\ ps ) }
13		df-rab	|- { x e. A | ph } = { x | ( x e. A /\ ph ) }
14		df-rab	|- { y e. A | ps } = { y | ( y e. A /\ ps ) }
15	12 13 14	3eqtr4i	|- { x e. A | ph } = { y e. A | ps }