Description: Obsolete version of cbvexv as of 11-Sep-2023. (Contributed by NM, 21-Jun-1993) Remove dependency on ax-10 . (Revised by Wolf Lammen, 17-Jul-2021) (Proof modification is discouraged.) (New usage is discouraged.)
| Ref | Expression | ||
|---|---|---|---|
| Hypothesis | cbvalv.1 | |- ( x = y -> ( ph <-> ps ) ) |
|
| Assertion | cbvexvOLD | |- ( E. x ph <-> E. y ps ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | cbvalv.1 | |- ( x = y -> ( ph <-> ps ) ) |
|
| 2 | 1 | notbid | |- ( x = y -> ( -. ph <-> -. ps ) ) |
| 3 | 2 | cbvalv | |- ( A. x -. ph <-> A. y -. ps ) |
| 4 | alnex | |- ( A. x -. ph <-> -. E. x ph ) |
|
| 5 | alnex | |- ( A. y -. ps <-> -. E. y ps ) |
|
| 6 | 3 4 5 | 3bitr3i | |- ( -. E. x ph <-> -. E. y ps ) |
| 7 | 6 | con4bii | |- ( E. x ph <-> E. y ps ) |