Metamath Proof Explorer


Theorem cbvrabv2w

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 }

Proof

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 }