Metamath Proof Explorer


Theorem bj-cbval2vv

Description: Version of cbval2vv with a disjoint variable condition, which does not require ax-13 . (Contributed by BJ, 16-Jun-2019) (Proof modification is discouraged.)

Ref Expression
Hypothesis bj-cbval2vv.1 x = z y = w φ ψ
Assertion bj-cbval2vv x y φ z w ψ

Proof

Step Hyp Ref Expression
1 bj-cbval2vv.1 x = z y = w φ ψ
2 nfv z φ
3 nfv w φ
4 nfv x ψ
5 nfv y ψ
6 2 3 4 5 1 cbval2v x y φ z w ψ