# Metamath Proof Explorer

## Theorem eupickbi

Description: Theorem *14.26 in WhiteheadRussell p. 192. (Contributed by Andrew Salmon, 11-Jul-2011) (Proof shortened by Wolf Lammen, 27-Dec-2018)

Ref Expression
Assertion eupickbi ${⊢}\exists !{x}\phantom{\rule{.4em}{0ex}}{\phi }\to \left(\exists {x}\phantom{\rule{.4em}{0ex}}\left({\phi }\wedge {\psi }\right)↔\forall {x}\phantom{\rule{.4em}{0ex}}\left({\phi }\to {\psi }\right)\right)$

### Proof

Step Hyp Ref Expression
1 eupicka ${⊢}\left(\exists !{x}\phantom{\rule{.4em}{0ex}}{\phi }\wedge \exists {x}\phantom{\rule{.4em}{0ex}}\left({\phi }\wedge {\psi }\right)\right)\to \forall {x}\phantom{\rule{.4em}{0ex}}\left({\phi }\to {\psi }\right)$
2 1 ex ${⊢}\exists !{x}\phantom{\rule{.4em}{0ex}}{\phi }\to \left(\exists {x}\phantom{\rule{.4em}{0ex}}\left({\phi }\wedge {\psi }\right)\to \forall {x}\phantom{\rule{.4em}{0ex}}\left({\phi }\to {\psi }\right)\right)$
3 euex ${⊢}\exists !{x}\phantom{\rule{.4em}{0ex}}{\phi }\to \exists {x}\phantom{\rule{.4em}{0ex}}{\phi }$
4 exintr ${⊢}\forall {x}\phantom{\rule{.4em}{0ex}}\left({\phi }\to {\psi }\right)\to \left(\exists {x}\phantom{\rule{.4em}{0ex}}{\phi }\to \exists {x}\phantom{\rule{.4em}{0ex}}\left({\phi }\wedge {\psi }\right)\right)$
5 3 4 syl5com ${⊢}\exists !{x}\phantom{\rule{.4em}{0ex}}{\phi }\to \left(\forall {x}\phantom{\rule{.4em}{0ex}}\left({\phi }\to {\psi }\right)\to \exists {x}\phantom{\rule{.4em}{0ex}}\left({\phi }\wedge {\psi }\right)\right)$
6 2 5 impbid ${⊢}\exists !{x}\phantom{\rule{.4em}{0ex}}{\phi }\to \left(\exists {x}\phantom{\rule{.4em}{0ex}}\left({\phi }\wedge {\psi }\right)↔\forall {x}\phantom{\rule{.4em}{0ex}}\left({\phi }\to {\psi }\right)\right)$