Description: Rule used to change bound variables, using implicit substitution. Version of cbvmo with a disjoint variable condition, which does not require ax-13 . (Contributed by NM, 9-Mar-1995) (Revised by Gino Giotto, 10-Jan-2024)
Ref | Expression | ||
---|---|---|---|
Hypotheses | cbvmow.1 | ||
cbvmow.2 | |||
cbvmow.3 | |||
Assertion | cbvmow |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | cbvmow.1 | ||
2 | cbvmow.2 | ||
3 | cbvmow.3 | ||
4 | 1 | sb8ev | |
5 | 1 | sb8euv | |
6 | 4 5 | imbi12i | |
7 | moeu | ||
8 | moeu | ||
9 | 6 7 8 | 3bitr4i | |
10 | 2 3 | sbiev | |
11 | 10 | mobii | |
12 | 9 11 | bitri |