Metamath Proof Explorer


Theorem cbvral2vw

Description: Version of cbvral2v with a disjoint variable condition, which does not require ax-13 . (Contributed by Gino Giotto, 10-Jan-2024)

Ref Expression
Hypotheses cbvral2vw.1 x = z φ χ
cbvral2vw.2 y = w χ ψ
Assertion cbvral2vw x A y B φ z A w B ψ

Proof

Step Hyp Ref Expression
1 cbvral2vw.1 x = z φ χ
2 cbvral2vw.2 y = w χ ψ
3 1 ralbidv x = z y B φ y B χ
4 3 cbvralvw x A y B φ z A y B χ
5 2 cbvralvw y B χ w B ψ
6 5 ralbii z A y B χ z A w B ψ
7 4 6 bitri x A y B φ z A w B ψ