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 }