# Metamath Proof Explorer

## Theorem nrexralim

Description: Negation of a complex predicate calculus formula. (Contributed by FL, 31-Jul-2009)

Ref Expression
Assertion nrexralim ${⊢}¬\exists {x}\in {A}\phantom{\rule{.4em}{0ex}}\forall {y}\in {B}\phantom{\rule{.4em}{0ex}}\left({\phi }\to {\psi }\right)↔\forall {x}\in {A}\phantom{\rule{.4em}{0ex}}\exists {y}\in {B}\phantom{\rule{.4em}{0ex}}\left({\phi }\wedge ¬{\psi }\right)$

### Proof

Step Hyp Ref Expression
1 rexanali ${⊢}\exists {y}\in {B}\phantom{\rule{.4em}{0ex}}\left({\phi }\wedge ¬{\psi }\right)↔¬\forall {y}\in {B}\phantom{\rule{.4em}{0ex}}\left({\phi }\to {\psi }\right)$
2 1 ralbii ${⊢}\forall {x}\in {A}\phantom{\rule{.4em}{0ex}}\exists {y}\in {B}\phantom{\rule{.4em}{0ex}}\left({\phi }\wedge ¬{\psi }\right)↔\forall {x}\in {A}\phantom{\rule{.4em}{0ex}}¬\forall {y}\in {B}\phantom{\rule{.4em}{0ex}}\left({\phi }\to {\psi }\right)$
3 ralnex ${⊢}\forall {x}\in {A}\phantom{\rule{.4em}{0ex}}¬\forall {y}\in {B}\phantom{\rule{.4em}{0ex}}\left({\phi }\to {\psi }\right)↔¬\exists {x}\in {A}\phantom{\rule{.4em}{0ex}}\forall {y}\in {B}\phantom{\rule{.4em}{0ex}}\left({\phi }\to {\psi }\right)$
4 2 3 bitr2i ${⊢}¬\exists {x}\in {A}\phantom{\rule{.4em}{0ex}}\forall {y}\in {B}\phantom{\rule{.4em}{0ex}}\left({\phi }\to {\psi }\right)↔\forall {x}\in {A}\phantom{\rule{.4em}{0ex}}\exists {y}\in {B}\phantom{\rule{.4em}{0ex}}\left({\phi }\wedge ¬{\psi }\right)$