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

Metamath Proof Explorer

Theorem cbvoprab3

Description: Rule used to change the third bound variable in an operation abstraction, using implicit substitution. (Contributed by NM, 22-Aug-2013)

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

Proof

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