Description: Theorem 19.12 of Margaris p. 89. Assuming the converse is a mistake sometimes made by beginners! But sometimes the converse does hold, as in 19.12vv and r19.12sn . (Contributed by NM, 12-Mar-1993) (Proof shortened by Wolf Lammen, 3-Jan-2018)
| Ref | Expression | ||
|---|---|---|---|
| Assertion | 19.12 | |- ( E. x A. y ph -> A. y E. x ph ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | nfa1 | |- F/ y A. y ph |
|
| 2 | 1 | nfex | |- F/ y E. x A. y ph |
| 3 | sp | |- ( A. y ph -> ph ) |
|
| 4 | 3 | eximi | |- ( E. x A. y ph -> E. x ph ) |
| 5 | 2 4 | alrimi | |- ( E. x A. y ph -> A. y E. x ph ) |