Description: Obsolete version of vtoclg as of 26-Jan-2025. (Contributed by NM, 17-Apr-1995) Avoid ax-12 . (Revised by SN, 20-Apr-2024) (New usage is discouraged.) (Proof modification is discouraged.)
| Ref | Expression | ||
|---|---|---|---|
| Hypotheses | vtoclg.1 | |- ( x = A -> ( ph <-> ps ) ) |
|
| vtoclg.2 | |- ph |
||
| Assertion | vtoclgOLD | |- ( A e. V -> ps ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | vtoclg.1 | |- ( x = A -> ( ph <-> ps ) ) |
|
| 2 | vtoclg.2 | |- ph |
|
| 3 | elisset | |- ( A e. V -> E. x x = A ) |
|
| 4 | 2 1 | mpbii | |- ( x = A -> ps ) |
| 5 | 4 | exlimiv | |- ( E. x x = A -> ps ) |
| 6 | 3 5 | syl | |- ( A e. V -> ps ) |