Description: Deduction used to change bound variables, using implicit substitution. Version of cbvexd with a disjoint variable condition, which does not require ax-13 . (Contributed by NM, 2-Jan-2002) (Revised by Gino Giotto, 10-Jan-2024)
| Ref | Expression | ||
|---|---|---|---|
| Hypotheses | cbvaldw.1 | |- F/ y ph |
|
| cbvaldw.2 | |- ( ph -> F/ y ps ) |
||
| cbvaldw.3 | |- ( ph -> ( x = y -> ( ps <-> ch ) ) ) |
||
| Assertion | cbvexdw | |- ( ph -> ( E. x ps <-> E. y ch ) ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | cbvaldw.1 | |- F/ y ph |
|
| 2 | cbvaldw.2 | |- ( ph -> F/ y ps ) |
|
| 3 | cbvaldw.3 | |- ( ph -> ( x = y -> ( ps <-> ch ) ) ) |
|
| 4 | 2 | nfnd | |- ( ph -> F/ y -. ps ) |
| 5 | notbi | |- ( ( ps <-> ch ) <-> ( -. ps <-> -. ch ) ) |
|
| 6 | 3 5 | syl6ib | |- ( ph -> ( x = y -> ( -. ps <-> -. ch ) ) ) |
| 7 | 1 4 6 | cbvaldw | |- ( ph -> ( A. x -. ps <-> A. y -. ch ) ) |
| 8 | alnex | |- ( A. x -. ps <-> -. E. x ps ) |
|
| 9 | alnex | |- ( A. y -. ch <-> -. E. y ch ) |
|
| 10 | 7 8 9 | 3bitr3g | |- ( ph -> ( -. E. x ps <-> -. E. y ch ) ) |
| 11 | 10 | con4bid | |- ( ph -> ( E. x ps <-> E. y ch ) ) |