This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem cbvoprab12v

Description: Rule used to change first two bound variables in an operation abstraction, using implicit substitution. (Contributed by NM, 8-Oct-2004)

Ref Expression
Hypothesis cbvoprab12v.1 
|- ( ( x = w /\ y = v ) -> ( ph <-> ps ) )
Assertion cbvoprab12v 
|- { <. <. x , y >. , z >. | ph } = { <. <. w , v >. , z >. | ps }

Proof

Step Hyp Ref Expression
1 cbvoprab12v.1 
 |-  ( ( x = w /\ y = v ) -> ( ph <-> ps ) )
2 opeq12 
 |-  ( ( x = w /\ y = v ) -> <. x , y >. = <. w , v >. )
3 2 opeq1d 
 |-  ( ( x = w /\ y = v ) -> <. <. x , y >. , z >. = <. <. w , v >. , z >. )
4 3 eqeq2d 
 |-  ( ( x = w /\ y = v ) -> ( u = <. <. x , y >. , z >. <-> u = <. <. w , v >. , z >. ) )
5 4 1 anbi12d 
 |-  ( ( x = w /\ y = v ) -> ( ( u = <. <. x , y >. , z >. /\ ph ) <-> ( u = <. <. w , v >. , z >. /\ ps ) ) )
6 5 exbidv 
 |-  ( ( x = w /\ y = v ) -> ( E. z ( u = <. <. x , y >. , z >. /\ ph ) <-> E. z ( u = <. <. w , v >. , z >. /\ ps ) ) )
7 6 cbvex2vw 
 |-  ( E. x E. y E. z ( u = <. <. x , y >. , z >. /\ ph ) <-> E. w E. v E. z ( u = <. <. w , v >. , z >. /\ ps ) )
8 7 abbii 
 |-  { u | E. x E. y E. z ( u = <. <. x , y >. , z >. /\ ph ) } = { u | E. w E. v E. z ( u = <. <. w , v >. , z >. /\ ps ) }
9 df-oprab 
 |-  { <. <. x , y >. , z >. | ph } = { u | E. x E. y E. z ( u = <. <. x , y >. , z >. /\ ph ) }
10 df-oprab 
 |-  { <. <. w , v >. , z >. | ps } = { u | E. w E. v E. z ( u = <. <. w , v >. , z >. /\ ps ) }
11 8 9 10 3eqtr4i 
 |-  { <. <. x , y >. , z >. | ph } = { <. <. w , v >. , z >. | ps }