Description: Rule used to change the third bound variable in an operation abstraction, using implicit substitution. (Contributed by NM, 8-Oct-2004) (Revised by David Abernethy, 19-Jun-2012)
Ref | Expression | ||
---|---|---|---|
Hypothesis | cbvoprab3v.1 | |- ( z = w -> ( ph <-> ps ) ) |
|
Assertion | cbvoprab3v | |- { <. <. x , y >. , z >. | ph } = { <. <. x , y >. , w >. | ps } |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | cbvoprab3v.1 | |- ( z = w -> ( ph <-> ps ) ) |
|
2 | nfv | |- F/ w ph |
|
3 | nfv | |- F/ z ps |
|
4 | 2 3 1 | cbvoprab3 | |- { <. <. x , y >. , z >. | ph } = { <. <. x , y >. , w >. | ps } |