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]˙ ψ

Proof

Step Hyp Ref Expression
1 cbvsbcvw.1 x = y φ ψ
2 1 cbvabv x | φ = y | ψ
3 2 eleq2i A x | φ A y | ψ
4 df-sbc [˙A / x]˙ φ A x | φ
5 df-sbc [˙A / y]˙ ψ A y | ψ
6 3 4 5 3bitr4i [˙A / x]˙ φ [˙A / y]˙ ψ