Description: Version of cbv2 with a disjoint variable condition, which does not require ax-13 . (Contributed by BJ, 16-Jun-2019) (Proof modification is discouraged.)
Ref | Expression | ||
---|---|---|---|
Hypotheses | bj-cbv2v.1 | |- F/ x ph |
|
bj-cbv2v.2 | |- F/ y ph |
||
bj-cbv2v.3 | |- ( ph -> F/ y ps ) |
||
bj-cbv2v.4 | |- ( ph -> F/ x ch ) |
||
bj-cbv2v.5 | |- ( ph -> ( x = y -> ( ps <-> ch ) ) ) |
||
Assertion | bj-cbv2v | |- ( ph -> ( A. x ps <-> A. y ch ) ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | bj-cbv2v.1 | |- F/ x ph |
|
2 | bj-cbv2v.2 | |- F/ y ph |
|
3 | bj-cbv2v.3 | |- ( ph -> F/ y ps ) |
|
4 | bj-cbv2v.4 | |- ( ph -> F/ x ch ) |
|
5 | bj-cbv2v.5 | |- ( ph -> ( x = y -> ( ps <-> ch ) ) ) |
|
6 | 2 | nf5ri | |- ( ph -> A. y ph ) |
7 | 1 | nfal | |- F/ x A. y ph |
8 | 7 | nf5ri | |- ( A. y ph -> A. x A. y ph ) |
9 | 6 8 | syl | |- ( ph -> A. x A. y ph ) |
10 | 3 | nf5rd | |- ( ph -> ( ps -> A. y ps ) ) |
11 | 4 | nf5rd | |- ( ph -> ( ch -> A. x ch ) ) |
12 | 10 11 5 | bj-cbv2hv | |- ( A. x A. y ph -> ( A. x ps <-> A. y ch ) ) |
13 | 9 12 | syl | |- ( ph -> ( A. x ps <-> A. y ch ) ) |