# Metamath Proof Explorer

## Theorem 0nelopab

Description: The empty set is never an element in an ordered-pair class abstraction. (Contributed by Alexander van der Vekens, 5-Nov-2017)

Ref Expression
Assertion 0nelopab ${⊢}¬\varnothing \in \left\{⟨{x},{y}⟩|{\phi }\right\}$

### Proof

Step Hyp Ref Expression
1 elopab ${⊢}\varnothing \in \left\{⟨{x},{y}⟩|{\phi }\right\}↔\exists {x}\phantom{\rule{.4em}{0ex}}\exists {y}\phantom{\rule{.4em}{0ex}}\left(\varnothing =⟨{x},{y}⟩\wedge {\phi }\right)$
2 nfopab1 ${⊢}\underset{_}{Ⅎ}{x}\phantom{\rule{.4em}{0ex}}\left\{⟨{x},{y}⟩|{\phi }\right\}$
3 2 nfel2 ${⊢}Ⅎ{x}\phantom{\rule{.4em}{0ex}}\varnothing \in \left\{⟨{x},{y}⟩|{\phi }\right\}$
4 3 nfn ${⊢}Ⅎ{x}\phantom{\rule{.4em}{0ex}}¬\varnothing \in \left\{⟨{x},{y}⟩|{\phi }\right\}$
5 nfopab2 ${⊢}\underset{_}{Ⅎ}{y}\phantom{\rule{.4em}{0ex}}\left\{⟨{x},{y}⟩|{\phi }\right\}$
6 5 nfel2 ${⊢}Ⅎ{y}\phantom{\rule{.4em}{0ex}}\varnothing \in \left\{⟨{x},{y}⟩|{\phi }\right\}$
7 6 nfn ${⊢}Ⅎ{y}\phantom{\rule{.4em}{0ex}}¬\varnothing \in \left\{⟨{x},{y}⟩|{\phi }\right\}$
8 vex ${⊢}{x}\in \mathrm{V}$
9 vex ${⊢}{y}\in \mathrm{V}$
10 8 9 opnzi ${⊢}⟨{x},{y}⟩\ne \varnothing$
11 nesym ${⊢}⟨{x},{y}⟩\ne \varnothing ↔¬\varnothing =⟨{x},{y}⟩$
12 pm2.21 ${⊢}¬\varnothing =⟨{x},{y}⟩\to \left(\varnothing =⟨{x},{y}⟩\to ¬\varnothing \in \left\{⟨{x},{y}⟩|{\phi }\right\}\right)$
13 11 12 sylbi ${⊢}⟨{x},{y}⟩\ne \varnothing \to \left(\varnothing =⟨{x},{y}⟩\to ¬\varnothing \in \left\{⟨{x},{y}⟩|{\phi }\right\}\right)$
14 10 13 ax-mp ${⊢}\varnothing =⟨{x},{y}⟩\to ¬\varnothing \in \left\{⟨{x},{y}⟩|{\phi }\right\}$
15 14 adantr ${⊢}\left(\varnothing =⟨{x},{y}⟩\wedge {\phi }\right)\to ¬\varnothing \in \left\{⟨{x},{y}⟩|{\phi }\right\}$
16 7 15 exlimi ${⊢}\exists {y}\phantom{\rule{.4em}{0ex}}\left(\varnothing =⟨{x},{y}⟩\wedge {\phi }\right)\to ¬\varnothing \in \left\{⟨{x},{y}⟩|{\phi }\right\}$
17 4 16 exlimi ${⊢}\exists {x}\phantom{\rule{.4em}{0ex}}\exists {y}\phantom{\rule{.4em}{0ex}}\left(\varnothing =⟨{x},{y}⟩\wedge {\phi }\right)\to ¬\varnothing \in \left\{⟨{x},{y}⟩|{\phi }\right\}$
18 1 17 sylbi ${⊢}\varnothing \in \left\{⟨{x},{y}⟩|{\phi }\right\}\to ¬\varnothing \in \left\{⟨{x},{y}⟩|{\phi }\right\}$
19 id ${⊢}¬\varnothing \in \left\{⟨{x},{y}⟩|{\phi }\right\}\to ¬\varnothing \in \left\{⟨{x},{y}⟩|{\phi }\right\}$
20 18 19 pm2.61i ${⊢}¬\varnothing \in \left\{⟨{x},{y}⟩|{\phi }\right\}$