Theorem axc7e

Abbreviated version of axc7 using the existential quantifier. Corresponds to the dual of Axiom (B) of modal logic. (Contributed by NM, 5-Aug-1993.) (Proof shortened by Wolf Lammen, 8-Jul-2022.)

Conclusion

\( \vdash \exists x \, \forall x \, \varphi \rightarrow \varphi \)

Proof

hbe1a

\( \vdash \exists x \, \forall x \, \varphi \rightarrow \forall x \, \varphi \)

19.21bi _