Metamath Proof Explorer


Theorem bj-cbvex2vv

Description: Version of cbvex2vv 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-cbval2vv.1
|- ( ( x = z /\ y = w ) -> ( ph <-> ps ) )
Assertion bj-cbvex2vv
|- ( E. x E. y ph <-> E. z E. w ps )

Proof

Step Hyp Ref Expression
1 bj-cbval2vv.1
 |-  ( ( x = z /\ y = w ) -> ( ph <-> ps ) )
2 nfv
 |-  F/ z ph
3 nfv
 |-  F/ w ph
4 nfv
 |-  F/ x ps
5 nfv
 |-  F/ y ps
6 2 3 4 5 1 cbvex2v
 |-  ( E. x E. y ph <-> E. z E. w ps )