Description: Version of cbval2vv 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-cbval2vv | |- ( A. x A. y ph <-> A. z A. 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 | cbval2v | |- ( A. x A. y ph <-> A. z A. w ps ) |