Theorem cbvoprab12

Description: Rule used to change first two bound variables in an operation abstraction, using implicit substitution. (Contributed by NM, 21-Feb-2004) (Proof shortened by Andrew Salmon, 22-Oct-2011)

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

Proof

Step	Hyp	Ref	Expression
1		cbvoprab12.1	|- F/ w ph
2		cbvoprab12.2	|- F/ v ph
3		cbvoprab12.3	|- F/ x ps
4		cbvoprab12.4	|- F/ y ps
5		cbvoprab12.5	|- ( ( x = w /\ y = v ) -> ( ph <-> ps ) )
6		nfv	|- F/ w u = <. x , y >.
7	6 1	nfan	|- F/ w ( u = <. x , y >. /\ ph )
8		nfv	|- F/ v u = <. x , y >.
9	8 2	nfan	|- F/ v ( u = <. x , y >. /\ ph )
10		nfv	|- F/ x u = <. w , v >.
11	10 3	nfan	|- F/ x ( u = <. w , v >. /\ ps )
12		nfv	|- F/ y u = <. w , v >.
13	12 4	nfan	|- F/ y ( u = <. w , v >. /\ ps )
14		opeq12	|- ( ( x = w /\ y = v ) -> <. x , y >. = <. w , v >. )
15	14	eqeq2d	|- ( ( x = w /\ y = v ) -> ( u = <. x , y >. <-> u = <. w , v >. ) )
16	15 5	anbi12d	|- ( ( x = w /\ y = v ) -> ( ( u = <. x , y >. /\ ph ) <-> ( u = <. w , v >. /\ ps ) ) )
17	7 9 11 13 16	cbvex2v	|- ( E. x E. y ( u = <. x , y >. /\ ph ) <-> E. w E. v ( u = <. w , v >. /\ ps ) )
18	17	opabbii	|- { <. u , z >. | E. x E. y ( u = <. x , y >. /\ ph ) } = { <. u , z >. | E. w E. v ( u = <. w , v >. /\ ps ) }
19		dfoprab2	|- { <. <. x , y >. , z >. | ph } = { <. u , z >. | E. x E. y ( u = <. x , y >. /\ ph ) }
20		dfoprab2	|- { <. <. w , v >. , z >. | ps } = { <. u , z >. | E. w E. v ( u = <. w , v >. /\ ps ) }
21	18 19 20	3eqtr4i	|- { <. <. x , y >. , z >. | ph } = { <. <. w , v >. , z >. | ps }