Theorem 19.43
Theorem 19.43 of [Margaris] p. 90. (Contributed by NM, 12-Mar-1993.)
(Proof shortened by Wolf Lammen, 27-Jun-2014.)
Conclusion
\( \vdash \exists x \, (\varphi \vee \psi) \leftrightarrow \exists x \, \varphi \vee \exists x \, \psi \)
Proof
df-or
l1
exbii _
\( \vdash \exists x \, (\varphi \vee \psi) \leftrightarrow \exists x \, (\neg \varphi \rightarrow \psi) \)
l2
19.35
\( \vdash \exists x \, (\neg \varphi \rightarrow \psi) \leftrightarrow \forall x \, \neg \varphi \rightarrow \exists x \, \psi \)
alnex
imbi1i _
\( \vdash \forall x \, \neg \varphi \rightarrow \exists x \, \psi \leftrightarrow \neg \exists x \, \varphi \rightarrow \exists x \, \psi \)
l5
3bitri l1 l2 _
\( \vdash \exists x \, (\varphi \vee \psi) \leftrightarrow \neg \exists x \, \varphi \rightarrow \exists x \, \psi \)
df-or
\( \vdash \exists x \, \varphi \vee \exists x \, \psi \leftrightarrow \neg \exists x \, \varphi \rightarrow \exists x \, \psi \)
bitr4i l5 _