Description: Change bound variable. Uses only Tarski's FOL axiom schemes. See cbvmo for a version with fewer disjoint variable conditions but requiring more axioms. (Contributed by NM, 9-Mar-1995) (Revised by Gino Giotto, 30-Sep-2024)
Ref | Expression | ||
---|---|---|---|
Hypothesis | cbvmovw.1 | ||
Assertion | cbvmovw |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | cbvmovw.1 | ||
2 | df-mo | ||
3 | equequ1 | ||
4 | 1 3 | imbi12d | |
5 | 4 | cbvalvw | |
6 | 5 | exbii | |
7 | df-mo | ||
8 | 7 | bicomi | |
9 | 2 6 8 | 3bitri |