Description: Deduction used to change bound variables, using implicit substitution, particularly useful in conjunction with dvelim . Usage of this theorem is discouraged because it depends on ax-13 . Use the weaker cbvexdw if possible. (Contributed by NM, 2-Jan-2002) (Revised by Mario Carneiro, 6-Oct-2016) (New usage is discouraged.)
| Ref | Expression | ||
|---|---|---|---|
| Hypotheses | cbvald.1 | |- F/ y ph |
|
| cbvald.2 | |- ( ph -> F/ y ps ) |
||
| cbvald.3 | |- ( ph -> ( x = y -> ( ps <-> ch ) ) ) |
||
| Assertion | cbvexd | |- ( ph -> ( E. x ps <-> E. y ch ) ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | cbvald.1 | |- F/ y ph |
|
| 2 | cbvald.2 | |- ( ph -> F/ y ps ) |
|
| 3 | cbvald.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 | cbvald | |- ( 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 ) ) |