Description: Changing a bound variable (universal quantification case) in a weak axiomatization, assuming that all variables denote (which is valid in inclusive free logic) and that equality is symmetric. (Contributed by BJ, 12-Mar-2023) (Proof modification is discouraged.)
Ref | Expression | ||
---|---|---|---|
Hypotheses | bj-cbval.denote | |- A. y E. x x = y |
|
bj-cbval.denote2 | |- A. x E. y y = x |
||
bj-cbval.maj | |- ( x = y -> ( ph <-> ps ) ) |
||
bj-cbval.equcomiv | |- ( y = x -> x = y ) |
||
Assertion | bj-cbval | |- ( A. x ph <-> A. y ps ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | bj-cbval.denote | |- A. y E. x x = y |
|
2 | bj-cbval.denote2 | |- A. x E. y y = x |
|
3 | bj-cbval.maj | |- ( x = y -> ( ph <-> ps ) ) |
|
4 | bj-cbval.equcomiv | |- ( y = x -> x = y ) |
|
5 | 3 | biimpd | |- ( x = y -> ( ph -> ps ) ) |
6 | 5 1 | bj-cbvalimi | |- ( A. x ph -> A. y ps ) |
7 | 3 | biimprd | |- ( x = y -> ( ps -> ph ) ) |
8 | 4 7 | syl | |- ( y = x -> ( ps -> ph ) ) |
9 | 8 2 | bj-cbvalimi | |- ( A. y ps -> A. x ph ) |
10 | 6 9 | impbii | |- ( A. x ph <-> A. y ps ) |