Metamath Proof Explorer


Theorem cbvrabv2

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 }

Proof

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 }