# Metamath Proof Explorer

## Theorem cbvexd

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 ) )`

### Proof

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 ) )`