Theorem cbvabw

Description: Rule used to change bound variables, using implicit substitution. Version of cbvab with a disjoint variable condition, which does not require ax-10 , ax-13 . (Contributed by Andrew Salmon, 11-Jul-2011) (Revised by Gino Giotto, 23-May-2024)

	Ref	Expression
Hypotheses	cbvabw.1	|- F/ y ph
	cbvabw.2	|- F/ x ps
	cbvabw.3	|- ( x = y -> ( ph <-> ps ) )
Assertion	cbvabw	|- { x | ph } = { y | ps }

Proof

Step	Hyp	Ref	Expression
1		cbvabw.1	|- F/ y ph
2		cbvabw.2	|- F/ x ps
3		cbvabw.3	|- ( x = y -> ( ph <-> ps ) )
4		nfv	|- F/ y x = w
5	4 1	nfim	|- F/ y ( x = w -> ph )
6		nfv	|- F/ x y = w
7	6 2	nfim	|- F/ x ( y = w -> ps )
8		equequ1	|- ( x = y -> ( x = w <-> y = w ) )
9	8 3	imbi12d	|- ( x = y -> ( ( x = w -> ph ) <-> ( y = w -> ps ) ) )
10	5 7 9	cbvalv1	|- ( A. x ( x = w -> ph ) <-> A. y ( y = w -> ps ) )
11	10	imbi2i	|- ( ( w = z -> A. x ( x = w -> ph ) ) <-> ( w = z -> A. y ( y = w -> ps ) ) )
12	11	albii	|- ( A. w ( w = z -> A. x ( x = w -> ph ) ) <-> A. w ( w = z -> A. y ( y = w -> ps ) ) )
13		df-sb	|- ( [ z / x ] ph <-> A. w ( w = z -> A. x ( x = w -> ph ) ) )
14		df-sb	|- ( [ z / y ] ps <-> A. w ( w = z -> A. y ( y = w -> ps ) ) )
15	12 13 14	3bitr4i	|- ( [ z / x ] ph <-> [ z / y ] ps )
16		df-clab	|- ( z e. { x | ph } <-> [ z / x ] ph )
17		df-clab	|- ( z e. { y | ps } <-> [ z / y ] ps )
18	15 16 17	3bitr4i	|- ( z e. { x | ph } <-> z e. { y | ps } )
19	18	eqriv	|- { x | ph } = { y | ps }