Description: Version of cbv3h with two disjoint variable conditions, which does not require ax-11 nor ax-13 . (Contributed by BJ, 24-Jun-2019) (Proof modification is discouraged.)
Ref | Expression | ||
---|---|---|---|
Hypotheses | bj-cbv3hv2.nf | |- ( ps -> A. x ps ) |
|
bj-cbv3hv2.1 | |- ( x = y -> ( ph -> ps ) ) |
||
Assertion | bj-cbv3hv2 | |- ( A. x ph -> A. y ps ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | bj-cbv3hv2.nf | |- ( ps -> A. x ps ) |
|
2 | bj-cbv3hv2.1 | |- ( x = y -> ( ph -> ps ) ) |
|
3 | 1 | nf5i | |- F/ x ps |
4 | 3 2 | cbv3v2 | |- ( A. x ph -> A. y ps ) |