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

Proof

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