Metamath Proof Explorer

Theorem ralnex2

Description: Relationship between two restricted universal and existential quantifiers. (Contributed by Glauco Siliprandi, 11-Dec-2019) (Proof shortened by Wolf Lammen, 18-May-2023)

Ref Expression
Assertion ralnex2 ${⊢}\forall {x}\in {A}\phantom{\rule{.4em}{0ex}}\forall {y}\in {B}\phantom{\rule{.4em}{0ex}}¬{\phi }↔¬\exists {x}\in {A}\phantom{\rule{.4em}{0ex}}\exists {y}\in {B}\phantom{\rule{.4em}{0ex}}{\phi }$

Proof

Step Hyp Ref Expression
1 ralnex ${⊢}\forall {y}\in {B}\phantom{\rule{.4em}{0ex}}¬{\phi }↔¬\exists {y}\in {B}\phantom{\rule{.4em}{0ex}}{\phi }$
2 1 ralbii ${⊢}\forall {x}\in {A}\phantom{\rule{.4em}{0ex}}\forall {y}\in {B}\phantom{\rule{.4em}{0ex}}¬{\phi }↔\forall {x}\in {A}\phantom{\rule{.4em}{0ex}}¬\exists {y}\in {B}\phantom{\rule{.4em}{0ex}}{\phi }$
3 ralnex ${⊢}\forall {x}\in {A}\phantom{\rule{.4em}{0ex}}¬\exists {y}\in {B}\phantom{\rule{.4em}{0ex}}{\phi }↔¬\exists {x}\in {A}\phantom{\rule{.4em}{0ex}}\exists {y}\in {B}\phantom{\rule{.4em}{0ex}}{\phi }$
4 2 3 bitri ${⊢}\forall {x}\in {A}\phantom{\rule{.4em}{0ex}}\forall {y}\in {B}\phantom{\rule{.4em}{0ex}}¬{\phi }↔¬\exists {x}\in {A}\phantom{\rule{.4em}{0ex}}\exists {y}\in {B}\phantom{\rule{.4em}{0ex}}{\phi }$