Metamath Proof Explorer


Theorem hbe1

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 )

Proof

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 )