Metamath Proof Explorer

Theorem cbvsbcvw

Description: Change the bound variable of a class substitution using implicit substitution. Version of cbvsbcv with a disjoint variable condition, which does not require ax-13 . (Contributed by NM, 30-Sep-2008) (Revised by Gino Giotto, 10-Jan-2024)

Ref Expression
Hypothesis cbvsbcvw.1 x = y φ ψ
Assertion cbvsbcvw [˙A / x]˙ φ [˙A / y]˙ ψ


Step Hyp Ref Expression
1 cbvsbcvw.1 x = y φ ψ
2 nfv y φ
3 nfv x ψ
4 2 3 1 cbvsbcw [˙A / x]˙ φ [˙A / y]˙ ψ