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