Description: A more general version of cbvrabv . Version of cbvrabv2 with a disjoint variable condition, which does not require ax-13 . (Contributed by Glauco Siliprandi, 23-Oct-2021) (Revised by Gino Giotto, 16-Apr-2024)
Ref | Expression | ||
---|---|---|---|
Hypotheses | cbvrabv2w.1 | |- ( x = y -> A = B ) |
|
cbvrabv2w.2 | |- ( x = y -> ( ph <-> ps ) ) |
||
Assertion | cbvrabv2w | |- { x e. A | ph } = { y e. B | ps } |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | cbvrabv2w.1 | |- ( x = y -> A = B ) |
|
2 | cbvrabv2w.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 | cbvrabcsfw | |- { x e. A | ph } = { y e. B | ps } |