Metamath Proof Explorer


Theorem bj-cbvexdv

Description: Version of cbvexd with a disjoint variable condition, which does not require ax-13 . (Contributed by BJ, 16-Jun-2019) (Proof modification is discouraged.)

Ref Expression
Hypotheses bj-cbvaldv.1
|- F/ y ph
bj-cbvaldv.2
|- ( ph -> F/ y ps )
bj-cbvaldv.3
|- ( ph -> ( x = y -> ( ps <-> ch ) ) )
Assertion bj-cbvexdv
|- ( ph -> ( E. x ps <-> E. y ch ) )

Proof

Step Hyp Ref Expression
1 bj-cbvaldv.1
 |-  F/ y ph
2 bj-cbvaldv.2
 |-  ( ph -> F/ y ps )
3 bj-cbvaldv.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 bj-cbvaldv
 |-  ( ph -> ( A. x -. ps <-> A. y -. ch ) )
8 7 notbid
 |-  ( ph -> ( -. A. x -. ps <-> -. A. y -. ch ) )
9 df-ex
 |-  ( E. x ps <-> -. A. x -. ps )
10 df-ex
 |-  ( E. y ch <-> -. A. y -. ch )
11 8 9 10 3bitr4g
 |-  ( ph -> ( E. x ps <-> E. y ch ) )