Description: A more general version of cbvrabv . Usage of this theorem is discouraged because it depends on ax-13 . Use of cbvrabv2w is preferred. (Contributed by Glauco Siliprandi, 23-Oct-2021) (New usage is discouraged.)
Ref | Expression | ||
---|---|---|---|
Hypotheses | cbvrabv2.1 | |- ( x = y -> A = B ) |
|
cbvrabv2.2 | |- ( x = y -> ( ph <-> ps ) ) |
||
Assertion | cbvrabv2 | |- { x e. A | ph } = { y e. B | ps } |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | cbvrabv2.1 | |- ( x = y -> A = B ) |
|
2 | cbvrabv2.2 | |- ( x = y -> ( ph <-> ps ) ) |
|
3 | nfcv | |- F/_ y A |
|
4 | nfcv | |- F/_ x B |
|
5 | nfv | |- F/ y ph |
|
6 | nfv | |- F/ x ps |
|
7 | 3 4 5 6 1 2 | cbvrabcsf | |- { x e. A | ph } = { y e. B | ps } |