Description: Change the bound variable of a restricted at-most-one quantifier using implicit substitution. Version of cbvrmo with a disjoint variable condition, which does not require ax-13 . (Contributed by NM, 16-Jun-2017) (Revised by Gino Giotto, 10-Jan-2024)
Ref | Expression | ||
---|---|---|---|
Hypotheses | cbvrmow.1 | ||
cbvrmow.2 | |||
cbvrmow.3 | |||
Assertion | cbvrmow |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | cbvrmow.1 | ||
2 | cbvrmow.2 | ||
3 | cbvrmow.3 | ||
4 | 1 2 3 | cbvrexw | |
5 | 1 2 3 | cbvreuw | |
6 | 4 5 | imbi12i | |
7 | rmo5 | ||
8 | rmo5 | ||
9 | 6 7 8 | 3bitr4i |