# Metamath Proof Explorer

## Theorem falseral0

Description: A false statement can only be true for elements of an empty set. (Contributed by AV, 30-Oct-2020)

Ref Expression
Assertion falseral0 ${⊢}\left(\forall {x}\phantom{\rule{.4em}{0ex}}¬{\phi }\wedge \forall {x}\in {A}\phantom{\rule{.4em}{0ex}}{\phi }\right)\to {A}=\varnothing$

### Proof

Step Hyp Ref Expression
1 df-ral ${⊢}\forall {x}\in {A}\phantom{\rule{.4em}{0ex}}{\phi }↔\forall {x}\phantom{\rule{.4em}{0ex}}\left({x}\in {A}\to {\phi }\right)$
2 19.26 ${⊢}\forall {x}\phantom{\rule{.4em}{0ex}}\left(¬{\phi }\wedge \left({x}\in {A}\to {\phi }\right)\right)↔\left(\forall {x}\phantom{\rule{.4em}{0ex}}¬{\phi }\wedge \forall {x}\phantom{\rule{.4em}{0ex}}\left({x}\in {A}\to {\phi }\right)\right)$
3 con3 ${⊢}\left({x}\in {A}\to {\phi }\right)\to \left(¬{\phi }\to ¬{x}\in {A}\right)$
4 3 impcom ${⊢}\left(¬{\phi }\wedge \left({x}\in {A}\to {\phi }\right)\right)\to ¬{x}\in {A}$
5 4 alimi ${⊢}\forall {x}\phantom{\rule{.4em}{0ex}}\left(¬{\phi }\wedge \left({x}\in {A}\to {\phi }\right)\right)\to \forall {x}\phantom{\rule{.4em}{0ex}}¬{x}\in {A}$
6 alnex ${⊢}\forall {x}\phantom{\rule{.4em}{0ex}}¬{x}\in {A}↔¬\exists {x}\phantom{\rule{.4em}{0ex}}{x}\in {A}$
7 5 6 sylib ${⊢}\forall {x}\phantom{\rule{.4em}{0ex}}\left(¬{\phi }\wedge \left({x}\in {A}\to {\phi }\right)\right)\to ¬\exists {x}\phantom{\rule{.4em}{0ex}}{x}\in {A}$
8 notnotb ${⊢}{A}=\varnothing ↔¬¬{A}=\varnothing$
9 neq0 ${⊢}¬{A}=\varnothing ↔\exists {x}\phantom{\rule{.4em}{0ex}}{x}\in {A}$
10 8 9 xchbinx ${⊢}{A}=\varnothing ↔¬\exists {x}\phantom{\rule{.4em}{0ex}}{x}\in {A}$
11 7 10 sylibr ${⊢}\forall {x}\phantom{\rule{.4em}{0ex}}\left(¬{\phi }\wedge \left({x}\in {A}\to {\phi }\right)\right)\to {A}=\varnothing$
12 2 11 sylbir ${⊢}\left(\forall {x}\phantom{\rule{.4em}{0ex}}¬{\phi }\wedge \forall {x}\phantom{\rule{.4em}{0ex}}\left({x}\in {A}\to {\phi }\right)\right)\to {A}=\varnothing$
13 1 12 sylan2b ${⊢}\left(\forall {x}\phantom{\rule{.4em}{0ex}}¬{\phi }\wedge \forall {x}\in {A}\phantom{\rule{.4em}{0ex}}{\phi }\right)\to {A}=\varnothing$