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 | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | nfv | |
|
2 | nfs1v | |
|
3 | sbequ12 | |
|
4 | 1 2 3 | cbvralw | |
5 | nfv | |
|
6 | nfv | |
|
7 | sbequ | |
|
8 | 5 6 7 | cbvralw | |
9 | 4 8 | bitri | |