Description: Version of cbv3 with two disjoint variable conditions, which does not require ax-11 nor ax-13 . (Contributed by BJ, 24-Jun-2019) (Proof shortened by Wolf Lammen, 30-Aug-2021)
| Ref | Expression | ||
|---|---|---|---|
| Hypotheses | cbv3v2.nf | |- F/ x ps |
|
| cbv3v2.1 | |- ( x = y -> ( ph -> ps ) ) |
||
| Assertion | cbv3v2 | |- ( A. x ph -> A. y ps ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | cbv3v2.nf | |- F/ x ps |
|
| 2 | cbv3v2.1 | |- ( x = y -> ( ph -> ps ) ) |
|
| 3 | 1 2 | spimfv | |- ( A. x ph -> ps ) |
| 4 | 3 | alrimiv | |- ( A. x ph -> A. y ps ) |