Description: Rule used to change bound variables, using implicit substitution. Usage of this theorem is discouraged because it depends on ax-13 . Check out cbvexvw , cbvexv1 for weaker versions requiring fewer axioms. (Contributed by NM, 21-Jun-1993) (New usage is discouraged.)
Ref | Expression | ||
---|---|---|---|
Hypotheses | cbval.1 | |- F/ y ph |
|
cbval.2 | |- F/ x ps |
||
cbval.3 | |- ( x = y -> ( ph <-> ps ) ) |
||
Assertion | cbvex | |- ( E. x ph <-> E. y ps ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | cbval.1 | |- F/ y ph |
|
2 | cbval.2 | |- F/ x ps |
|
3 | cbval.3 | |- ( x = y -> ( ph <-> ps ) ) |
|
4 | 1 | nfn | |- F/ y -. ph |
5 | 2 | nfn | |- F/ x -. ps |
6 | 3 | notbid | |- ( x = y -> ( -. ph <-> -. ps ) ) |
7 | 4 5 6 | cbval | |- ( A. x -. ph <-> A. y -. ps ) |
8 | alnex | |- ( A. x -. ph <-> -. E. x ph ) |
|
9 | alnex | |- ( A. y -. ps <-> -. E. y ps ) |
|
10 | 7 8 9 | 3bitr3i | |- ( -. E. x ph <-> -. E. y ps ) |
11 | 10 | con4bii | |- ( E. x ph <-> E. y ps ) |