Description: A more efficient proof of Theorem 9.26 of Clemente p. 45. Compare with ex-natded9.26 . (Contributed by Mario Carneiro, 9-Feb-2017) (Proof modification is discouraged.) (New usage is discouraged.)
| Ref | Expression | ||
|---|---|---|---|
| Hypothesis | ex-natded9.26.1 | |- ( ph -> E. x A. y ps ) |
|
| Assertion | ex-natded9.26-2 | |- ( ph -> A. y E. x ps ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | ex-natded9.26.1 | |- ( ph -> E. x A. y ps ) |
|
| 2 | sp | |- ( A. y ps -> ps ) |
|
| 3 | 2 | eximi | |- ( E. x A. y ps -> E. x ps ) |
| 4 | 1 3 | syl | |- ( ph -> E. x ps ) |
| 5 | 4 | alrimiv | |- ( ph -> A. y E. x ps ) |