Metamath Proof Explorer


Theorem cbvexdw

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

Proof

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