Metamath Proof Explorer


Theorem cbvralsvw

Description: Change bound variable by using a substitution. Version of cbvralsv with a disjoint variable condition, which does not require ax-13 . (Contributed by NM, 20-Nov-2005) (Revised by Gino Giotto, 10-Jan-2024)

Ref Expression
Assertion cbvralsvw xAφyAyxφ

Proof

Step Hyp Ref Expression
1 nfv zφ
2 nfs1v xzxφ
3 sbequ12 x=zφzxφ
4 1 2 3 cbvralw xAφzAzxφ
5 nfv yzxφ
6 nfv zyxφ
7 sbequ z=yzxφyxφ
8 5 6 7 cbvralw zAzxφyAyxφ
9 4 8 bitri xAφyAyxφ