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 x A φ y A y x φ


Step Hyp Ref Expression
1 nfv z φ
2 nfs1v x z x φ
3 sbequ12 x = z φ z x φ
4 1 2 3 cbvralw x A φ z A z x φ
5 nfv y z x φ
6 nfv z y x φ
7 sbequ z = y z x φ y x φ
8 5 6 7 cbvralw z A z x φ y A y x φ
9 4 8 bitri x A φ y A y x φ