Theorem cbvrab

Description: Rule to change the bound variable in a restricted class abstraction, using implicit substitution. This version has bound-variable hypotheses in place of distinct variable conditions. Usage of this theorem is discouraged because it depends on ax-13 . Use the weaker cbvrabw when possible. (Contributed by Andrew Salmon, 11-Jul-2011) (Revised by Mario Carneiro, 9-Oct-2016) (New usage is discouraged.)

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

Proof

Step	Hyp	Ref	Expression
1		cbvrab.1	|- F/_ x A
2		cbvrab.2	|- F/_ y A
3		cbvrab.3	|- F/ y ph
4		cbvrab.4	|- F/ x ps
5		cbvrab.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	cbvab	|- { x | ( x e. A /\ ph ) } = { z | ( z e. A /\ [ z / x ] ph ) }
14	2	nfcri	|- F/ y z e. A
15	3	nfsb	|- 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	sbie	|- ( [ 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	cbvab	|- { 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 }