Description: Closed form of 19.9 and version of 19.3t with an existential quantifier. (Contributed by NM, 13-May-1993) (Revised by Mario Carneiro, 24-Sep-2016) (Proof shortened by Wolf Lammen, 14-Jul-2020)
| Ref | Expression | ||
|---|---|---|---|
| Assertion | 19.9t | |- ( F/ x ph -> ( E. x ph <-> ph ) ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | id | |- ( F/ x ph -> F/ x ph ) |
|
| 2 | 1 | 19.9d | |- ( F/ x ph -> ( E. x ph -> ph ) ) |
| 3 | 19.8a | |- ( ph -> E. x ph ) |
|
| 4 | 2 3 | impbid1 | |- ( F/ x ph -> ( E. x ph <-> ph ) ) |