Description: Rule used to change bound variables in an ordered-pair class abstraction, using implicit substitution. (Contributed by NM, 15-Oct-1996)
Ref | Expression | ||
---|---|---|---|
Hypothesis | cbvopabv.1 | |- ( ( x = z /\ y = w ) -> ( ph <-> ps ) ) |
|
Assertion | cbvopabv | |- { <. x , y >. | ph } = { <. z , w >. | ps } |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | cbvopabv.1 | |- ( ( x = z /\ y = w ) -> ( ph <-> ps ) ) |
|
2 | nfv | |- F/ z ph |
|
3 | nfv | |- F/ w ph |
|
4 | nfv | |- F/ x ps |
|
5 | nfv | |- F/ y ps |
|
6 | 2 3 4 5 1 | cbvopab | |- { <. x , y >. | ph } = { <. z , w >. | ps } |