Theorem cbvoprab1

Description: Rule used to change first bound variable in an operation abstraction, using implicit substitution. (Contributed by NM, 20-Dec-2008) (Revised by Mario Carneiro, 5-Dec-2016)

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

Proof

Step	Hyp	Ref	Expression
1		cbvoprab1.1	|- F/ w ph
2		cbvoprab1.2	|- F/ x ps
3		cbvoprab1.3	|- ( x = 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		nfv	|- F/ x v = <. w , y >.
8	7 2	nfan	|- F/ x ( v = <. w , y >. /\ ps )
9	8	nfex	|- F/ x E. y ( v = <. w , y >. /\ ps )
10		opeq1	|- ( x = w -> <. x , y >. = <. w , y >. )
11	10	eqeq2d	|- ( x = w -> ( v = <. x , y >. <-> v = <. w , y >. ) )
12	11 3	anbi12d	|- ( x = w -> ( ( v = <. x , y >. /\ ph ) <-> ( v = <. w , y >. /\ ps ) ) )
13	12	exbidv	|- ( x = w -> ( E. y ( v = <. x , y >. /\ ph ) <-> E. y ( v = <. w , y >. /\ ps ) ) )
14	6 9 13	cbvexv1	|- ( E. x E. y ( v = <. x , y >. /\ ph ) <-> E. w E. y ( v = <. w , y >. /\ ps ) )
15	14	opabbii	|- { <. v , z >. | E. x E. y ( v = <. x , y >. /\ ph ) } = { <. v , z >. | E. w E. y ( v = <. w , y >. /\ ps ) }
16		dfoprab2	|- { <. <. x , y >. , z >. | ph } = { <. v , z >. | E. x E. y ( v = <. x , y >. /\ ph ) }
17		dfoprab2	|- { <. <. w , y >. , z >. | ps } = { <. v , z >. | E. w E. y ( v = <. w , y >. /\ ps ) }
18	15 16 17	3eqtr4i	|- { <. <. x , y >. , z >. | ph } = { <. <. w , y >. , z >. | ps }