Metamath Proof Explorer


Theorem cbvoprab2

Description: Change the second bound variable in an operation abstraction. (Contributed by Jeff Madsen, 11-Jun-2010) (Revised by Mario Carneiro, 11-Dec-2016)

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

Proof

Step Hyp Ref Expression
1 cbvoprab2.1
 |-  F/ w ph
2 cbvoprab2.2
 |-  F/ y ps
3 cbvoprab2.3
 |-  ( y = w -> ( ph <-> ps ) )
4 nfv
 |-  F/ w v = <. <. x , y >. , z >.
5 4 1 nfan
 |-  F/ w ( v = <. <. x , y >. , z >. /\ ph )
6 5 nfex
 |-  F/ w E. z ( v = <. <. x , y >. , z >. /\ ph )
7 nfv
 |-  F/ y v = <. <. x , w >. , z >.
8 7 2 nfan
 |-  F/ y ( v = <. <. x , w >. , z >. /\ ps )
9 8 nfex
 |-  F/ y E. z ( v = <. <. x , w >. , z >. /\ ps )
10 opeq2
 |-  ( y = w -> <. x , y >. = <. x , w >. )
11 10 opeq1d
 |-  ( y = w -> <. <. x , y >. , z >. = <. <. x , w >. , z >. )
12 11 eqeq2d
 |-  ( y = w -> ( v = <. <. x , y >. , z >. <-> v = <. <. x , w >. , z >. ) )
13 12 3 anbi12d
 |-  ( y = w -> ( ( v = <. <. x , y >. , z >. /\ ph ) <-> ( v = <. <. x , w >. , z >. /\ ps ) ) )
14 13 exbidv
 |-  ( y = w -> ( E. z ( v = <. <. x , y >. , z >. /\ ph ) <-> E. z ( v = <. <. x , w >. , z >. /\ ps ) ) )
15 6 9 14 cbvexv1
 |-  ( E. y E. z ( v = <. <. x , y >. , z >. /\ ph ) <-> E. w E. z ( v = <. <. x , w >. , z >. /\ ps ) )
16 15 exbii
 |-  ( E. x E. y E. z ( v = <. <. x , y >. , z >. /\ ph ) <-> E. x E. w E. z ( v = <. <. x , w >. , z >. /\ ps ) )
17 16 abbii
 |-  { v | E. x E. y E. z ( v = <. <. x , y >. , z >. /\ ph ) } = { v | E. x E. w E. z ( v = <. <. x , w >. , z >. /\ ps ) }
18 df-oprab
 |-  { <. <. x , y >. , z >. | ph } = { v | E. x E. y E. z ( v = <. <. x , y >. , z >. /\ ph ) }
19 df-oprab
 |-  { <. <. x , w >. , z >. | ps } = { v | E. x E. w E. z ( v = <. <. x , w >. , z >. /\ ps ) }
20 17 18 19 3eqtr4i
 |-  { <. <. x , y >. , z >. | ph } = { <. <. x , w >. , z >. | ps }