Description: Changing a bound variable (existential 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-cbvex | |- ( E. x ph <-> E. 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 | 4 5 | syl | |- ( y = x -> ( ph -> ps ) ) |
7 | 6 2 | bj-cbveximi | |- ( E. x ph -> E. y ps ) |
8 | 3 | biimprd | |- ( x = y -> ( ps -> ph ) ) |
9 | 8 1 | bj-cbveximi | |- ( E. y ps -> E. x ph ) |
10 | 7 9 | impbii | |- ( E. x ph <-> E. y ps ) |