Metamath Proof Explorer


Theorem bj-cbvexdvav

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

Ref Expression
Hypothesis bj-cbvaldvav.1
|- ( ( ph /\ x = y ) -> ( ps <-> ch ) )
Assertion bj-cbvexdvav
|- ( ph -> ( E. x ps <-> E. y ch ) )

Proof

Step Hyp Ref Expression
1 bj-cbvaldvav.1
 |-  ( ( ph /\ x = y ) -> ( ps <-> ch ) )
2 nfv
 |-  F/ y ph
3 nfvd
 |-  ( ph -> F/ y ps )
4 1 ex
 |-  ( ph -> ( x = y -> ( ps <-> ch ) ) )
5 2 3 4 bj-cbvexdv
 |-  ( ph -> ( E. x ps <-> E. y ch ) )