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	$$⊢\neg \varnothing \in \left\{⟨x,y⟩|\phi \right\}$$

Proof

Step	Hyp	Ref	Expression
1		elopab	$$⊢\varnothing \in \left\{⟨x,y⟩|\phi \right\}\leftrightarrow \exists x\exists y\left(\varnothing =⟨x,y⟩\wedge \phi \right)$$
2		nfopab1	$$⊢\underset{\_}{Ⅎ}x\left\{⟨x,y⟩|\phi \right\}$$
3	2	nfel2	$$⊢Ⅎx\varnothing \in \left\{⟨x,y⟩|\phi \right\}$$
4	3	nfn	$$⊢Ⅎx\neg \varnothing \in \left\{⟨x,y⟩|\phi \right\}$$
5		nfopab2	$$⊢\underset{\_}{Ⅎ}y\left\{⟨x,y⟩|\phi \right\}$$
6	5	nfel2	$$⊢Ⅎy\varnothing \in \left\{⟨x,y⟩|\phi \right\}$$
7	6	nfn	$$⊢Ⅎy\neg \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 \leftrightarrow \neg \varnothing =⟨x,y⟩$$
12		pm2.21	$$⊢\neg \varnothing =⟨x,y⟩\to \left(\varnothing =⟨x,y⟩\to \neg \varnothing \in \left\{⟨x,y⟩|\phi \right\}\right)$$
13	11 12	sylbi	$$⊢⟨x,y⟩\ne \varnothing \to \left(\varnothing =⟨x,y⟩\to \neg \varnothing \in \left\{⟨x,y⟩|\phi \right\}\right)$$
14	10 13	ax-mp	$$⊢\varnothing =⟨x,y⟩\to \neg \varnothing \in \left\{⟨x,y⟩|\phi \right\}$$
15	14	adantr	$$⊢\left(\varnothing =⟨x,y⟩\wedge \phi \right)\to \neg \varnothing \in \left\{⟨x,y⟩|\phi \right\}$$
16	7 15	exlimi	$$⊢\exists y\left(\varnothing =⟨x,y⟩\wedge \phi \right)\to \neg \varnothing \in \left\{⟨x,y⟩|\phi \right\}$$
17	4 16	exlimi	$$⊢\exists x\exists y\left(\varnothing =⟨x,y⟩\wedge \phi \right)\to \neg \varnothing \in \left\{⟨x,y⟩|\phi \right\}$$
18	1 17	sylbi	$$⊢\varnothing \in \left\{⟨x,y⟩|\phi \right\}\to \neg \varnothing \in \left\{⟨x,y⟩|\phi \right\}$$
19		id	$$⊢\neg \varnothing \in \left\{⟨x,y⟩|\phi \right\}\to \neg \varnothing \in \left\{⟨x,y⟩|\phi \right\}$$
20	18 19	pm2.61i	$$⊢\neg \varnothing \in \left\{⟨x,y⟩|\phi \right\}$$