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 }

Metamath Proof Explorer

Theorem cbvoprab12

Proof