Theorem cbvoprab3

Description: Rule used to change the third bound variable in an operation abstraction, using implicit substitution. (Contributed by NM, 22-Aug-2013)

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

Proof

Step	Hyp	Ref	Expression
1		cbvoprab3.1	|- F/ w ph
2		cbvoprab3.2	|- F/ z ps
3		cbvoprab3.3	|- ( z = w -> ( ph <-> ps ) )
4		nfv	|- F/ w v = <. x , y >.
5	4 1	nfan	|- F/ w ( v = <. x , y >. /\ ph )
6	5	nfex	|- F/ w E. y ( v = <. x , y >. /\ ph )
7	6	nfex	|- F/ w E. x E. y ( v = <. x , y >. /\ ph )
8		nfv	|- F/ z v = <. x , y >.
9	8 2	nfan	|- F/ z ( v = <. x , y >. /\ ps )
10	9	nfex	|- F/ z E. y ( v = <. x , y >. /\ ps )
11	10	nfex	|- F/ z E. x E. y ( v = <. x , y >. /\ ps )
12	3	anbi2d	|- ( z = w -> ( ( v = <. x , y >. /\ ph ) <-> ( v = <. x , y >. /\ ps ) ) )
13	12	2exbidv	|- ( z = w -> ( E. x E. y ( v = <. x , y >. /\ ph ) <-> E. x E. y ( v = <. x , y >. /\ ps ) ) )
14	7 11 13	cbvopab2	|- { <. v , z >. | E. x E. y ( v = <. x , y >. /\ ph ) } = { <. v , w >. | E. x E. y ( v = <. x , y >. /\ ps ) }
15		dfoprab2	|- { <. <. x , y >. , z >. | ph } = { <. v , z >. | E. x E. y ( v = <. x , y >. /\ ph ) }
16		dfoprab2	|- { <. <. x , y >. , w >. | ps } = { <. v , w >. | E. x E. y ( v = <. x , y >. /\ ps ) }
17	14 15 16	3eqtr4i	|- { <. <. x , y >. , z >. | ph } = { <. <. x , y >. , w >. | ps }