Metamath Proof Explorer

Theorem cbvrexsvw

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

Ref Expression
Assertion cbvrexsvw 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 cbvrexw 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 cbvrexw z A z x φ y A y x φ
9 4 8 bitri x A φ y A y x φ