Description: Version of spvw and 19.3v proved from ax-1 -- ax-5 . The antecedent can for instance be proved with the existence axiom extru . (Contributed by BJ, 8-Mar-2026) (Proof modification is discouraged.)
| Ref | Expression | ||
|---|---|---|---|
| Assertion | bj-spvw | |- ( E. x ph -> ( ps <-> A. x ps ) ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | ax-5 | |- ( ps -> A. x ps ) |
|
| 2 | bj-axdd2 | |- ( E. x ph -> ( A. x ps -> E. x ps ) ) |
|
| 3 | ax5e | |- ( E. x ps -> ps ) |
|
| 4 | 2 3 | syl6 | |- ( E. x ph -> ( A. x ps -> ps ) ) |
| 5 | 1 4 | impbid2 | |- ( E. x ph -> ( ps <-> A. x ps ) ) |