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) (Revised by Gino Giotto, 10-Jan-2024)

	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		nfv	|- F/ z ( x e. A /\ ph )
7	1	nfcri	|- F/ x z e. A
8		nfs1v	|- F/ x [ z / x ] ph
9	7 8	nfan	|- F/ x ( z e. A /\ [ z / x ] ph )
10		eleq1w	|- ( x = z -> ( x e. A <-> z e. A ) )
11		sbequ12	|- ( x = z -> ( ph <-> [ z / x ] ph ) )
12	10 11	anbi12d	|- ( x = z -> ( ( x e. A /\ ph ) <-> ( z e. A /\ [ z / x ] ph ) ) )
13	6 9 12	cbvabw	|- { x | ( x e. A /\ ph ) } = { z | ( z e. A /\ [ z / x ] ph ) }
14	2	nfcri	|- F/ y z e. A
15	3	nfsbv	|- F/ y [ z / x ] ph
16	14 15	nfan	|- F/ y ( z e. A /\ [ z / x ] ph )
17		nfv	|- F/ z ( y e. A /\ ps )
18		eleq1w	|- ( z = y -> ( z e. A <-> y e. A ) )
19		sbequ	|- ( z = y -> ( [ z / x ] ph <-> [ y / x ] ph ) )
20	4 5	sbiev	|- ( [ y / x ] ph <-> ps )
21	19 20	bitrdi	|- ( z = y -> ( [ z / x ] ph <-> ps ) )
22	18 21	anbi12d	|- ( z = y -> ( ( z e. A /\ [ z / x ] ph ) <-> ( y e. A /\ ps ) ) )
23	16 17 22	cbvabw	|- { z | ( z e. A /\ [ z / x ] ph ) } = { y | ( y e. A /\ ps ) }
24	13 23	eqtri	|- { x | ( x e. A /\ ph ) } = { y | ( y e. A /\ ps ) }
25		df-rab	|- { x e. A | ph } = { x | ( x e. A /\ ph ) }
26		df-rab	|- { y e. A | ps } = { y | ( y e. A /\ ps ) }
27	24 25 26	3eqtr4i	|- { x e. A | ph } = { y e. A | ps }