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 ) ) |