Description: The setvar x is not free in E. x ph . Corresponds to the axiom (5) of modal logic (see also modal5 ). (Contributed by NM, 24-Jan-1993)
Ref | Expression | ||
---|---|---|---|
Assertion | hbe1 | |- ( E. x ph -> A. x E. x ph ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | df-ex | |- ( E. x ph <-> -. A. x -. ph ) |
|
2 | hbn1 | |- ( -. A. x -. ph -> A. x -. A. x -. ph ) |
|
3 | 1 2 | hbxfrbi | |- ( E. x ph -> A. x E. x ph ) |