# Metamath Proof Explorer

## Theorem 19.43

Description: Theorem 19.43 of Margaris p. 90. (Contributed by NM, 12-Mar-1993) (Proof shortened by Wolf Lammen, 27-Jun-2014)

Ref Expression
Assertion 19.43 ${⊢}\exists {x}\phantom{\rule{.4em}{0ex}}\left({\phi }\vee {\psi }\right)↔\left(\exists {x}\phantom{\rule{.4em}{0ex}}{\phi }\vee \exists {x}\phantom{\rule{.4em}{0ex}}{\psi }\right)$

### Proof

Step Hyp Ref Expression
1 df-or ${⊢}\left({\phi }\vee {\psi }\right)↔\left(¬{\phi }\to {\psi }\right)$
2 1 exbii ${⊢}\exists {x}\phantom{\rule{.4em}{0ex}}\left({\phi }\vee {\psi }\right)↔\exists {x}\phantom{\rule{.4em}{0ex}}\left(¬{\phi }\to {\psi }\right)$
3 19.35 ${⊢}\exists {x}\phantom{\rule{.4em}{0ex}}\left(¬{\phi }\to {\psi }\right)↔\left(\forall {x}\phantom{\rule{.4em}{0ex}}¬{\phi }\to \exists {x}\phantom{\rule{.4em}{0ex}}{\psi }\right)$
4 alnex ${⊢}\forall {x}\phantom{\rule{.4em}{0ex}}¬{\phi }↔¬\exists {x}\phantom{\rule{.4em}{0ex}}{\phi }$
5 4 imbi1i ${⊢}\left(\forall {x}\phantom{\rule{.4em}{0ex}}¬{\phi }\to \exists {x}\phantom{\rule{.4em}{0ex}}{\psi }\right)↔\left(¬\exists {x}\phantom{\rule{.4em}{0ex}}{\phi }\to \exists {x}\phantom{\rule{.4em}{0ex}}{\psi }\right)$
6 2 3 5 3bitri ${⊢}\exists {x}\phantom{\rule{.4em}{0ex}}\left({\phi }\vee {\psi }\right)↔\left(¬\exists {x}\phantom{\rule{.4em}{0ex}}{\phi }\to \exists {x}\phantom{\rule{.4em}{0ex}}{\psi }\right)$
7 df-or ${⊢}\left(\exists {x}\phantom{\rule{.4em}{0ex}}{\phi }\vee \exists {x}\phantom{\rule{.4em}{0ex}}{\psi }\right)↔\left(¬\exists {x}\phantom{\rule{.4em}{0ex}}{\phi }\to \exists {x}\phantom{\rule{.4em}{0ex}}{\psi }\right)$
8 6 7 bitr4i ${⊢}\exists {x}\phantom{\rule{.4em}{0ex}}\left({\phi }\vee {\psi }\right)↔\left(\exists {x}\phantom{\rule{.4em}{0ex}}{\phi }\vee \exists {x}\phantom{\rule{.4em}{0ex}}{\psi }\right)$