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 ( 𝑥 = 𝑦𝐴 = 𝐵 )
cbvrabv2.2 ( 𝑥 = 𝑦 → ( 𝜑𝜓 ) )
Assertion cbvrabv2 { 𝑥𝐴𝜑 } = { 𝑦𝐵𝜓 }

Proof

Step Hyp Ref Expression
1 cbvrabv2.1 ( 𝑥 = 𝑦𝐴 = 𝐵 )
2 cbvrabv2.2 ( 𝑥 = 𝑦 → ( 𝜑𝜓 ) )
3 nfcv 𝑦 𝐴
4 nfcv 𝑥 𝐵
5 nfv 𝑦 𝜑
6 nfv 𝑥 𝜓
7 3 4 5 6 1 2 cbvrabcsf { 𝑥𝐴𝜑 } = { 𝑦𝐵𝜓 }