Metamath Proof Explorer

Theorem cbvex2vw

Description: Rule used to change bound variables, using implicit substitution. Version of cbvex2vv with more disjoint variable conditions, which requires fewer axioms . (Contributed by NM, 26-Jul-1995) (Revised by Gino Giotto, 10-Jan-2024)

Ref Expression
Hypothesis cbval2vw.1 x = z y = w φ ψ
Assertion cbvex2vw x y φ z w ψ


Step Hyp Ref Expression
1 cbval2vw.1 x = z y = w φ ψ
2 1 cbvexdvaw x = z y φ w ψ
3 2 cbvexvw x y φ z w ψ