Description: Change bound variables of triple restricted universal quantification, using implicit substitution. Version of cbvral3v with a disjoint variable condition, which does not require ax-13 . (Contributed by NM, 10-May-2005) (Revised by Gino Giotto, 10-Jan-2024)
| Ref | Expression | ||
|---|---|---|---|
| Hypotheses | cbvral3vw.1 | |- ( x = w -> ( ph <-> ch ) ) |
|
| cbvral3vw.2 | |- ( y = v -> ( ch <-> th ) ) |
||
| cbvral3vw.3 | |- ( z = u -> ( th <-> ps ) ) |
||
| Assertion | cbvral3vw | |- ( A. x e. A A. y e. B A. z e. C ph <-> A. w e. A A. v e. B A. u e. C ps ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | cbvral3vw.1 | |- ( x = w -> ( ph <-> ch ) ) |
|
| 2 | cbvral3vw.2 | |- ( y = v -> ( ch <-> th ) ) |
|
| 3 | cbvral3vw.3 | |- ( z = u -> ( th <-> ps ) ) |
|
| 4 | 1 | 2ralbidv | |- ( x = w -> ( A. y e. B A. z e. C ph <-> A. y e. B A. z e. C ch ) ) |
| 5 | 4 | cbvralvw | |- ( A. x e. A A. y e. B A. z e. C ph <-> A. w e. A A. y e. B A. z e. C ch ) |
| 6 | 2 3 | cbvral2vw | |- ( A. y e. B A. z e. C ch <-> A. v e. B A. u e. C ps ) |
| 7 | 6 | ralbii | |- ( A. w e. A A. y e. B A. z e. C ch <-> A. w e. A A. v e. B A. u e. C ps ) |
| 8 | 5 7 | bitri | |- ( A. x e. A A. y e. B A. z e. C ph <-> A. w e. A A. v e. B A. u e. C ps ) |