Theorem spr0nelg

Description: The empty set is not an element of all unordered pairs. (Contributed by AV, 21-Nov-2021)

	Ref	Expression
Assertion	spr0nelg	$$⊢\varnothing \notin \left\{p|\exists a\exists bp=\left\{a,b\right\}\right\}$$

Proof

Step	Hyp	Ref	Expression
1		ianor	$$⊢\neg \left(p=\varnothing \wedge \exists a\exists bp=\left\{a,b\right\}\right)\leftrightarrow \left(\neg p=\varnothing \vee \neg \exists a\exists bp=\left\{a,b\right\}\right)$$
2	1	bicomi	$$⊢\left(\neg p=\varnothing \vee \neg \exists a\exists bp=\left\{a,b\right\}\right)\leftrightarrow \neg \left(p=\varnothing \wedge \exists a\exists bp=\left\{a,b\right\}\right)$$
3	2	albii	$$⊢\forall p\left(\neg p=\varnothing \vee \neg \exists a\exists bp=\left\{a,b\right\}\right)\leftrightarrow \forall p\neg \left(p=\varnothing \wedge \exists a\exists bp=\left\{a,b\right\}\right)$$
4		alnex	$$⊢\forall p\neg \left(p=\varnothing \wedge \exists a\exists bp=\left\{a,b\right\}\right)\leftrightarrow \neg \exists p\left(p=\varnothing \wedge \exists a\exists bp=\left\{a,b\right\}\right)$$
5	3 4	bitri	$$⊢\forall p\left(\neg p=\varnothing \vee \neg \exists a\exists bp=\left\{a,b\right\}\right)\leftrightarrow \neg \exists p\left(p=\varnothing \wedge \exists a\exists bp=\left\{a,b\right\}\right)$$
6		vex	$$⊢a\in \mathrm{V}$$
7	6	prnz	$$⊢\left\{a,b\right\}\ne \varnothing$$
8	7	nesymi	$$⊢\neg \varnothing =\left\{a,b\right\}$$
9		eqeq1	$$⊢p=\varnothing \to \left(p=\left\{a,b\right\}\leftrightarrow \varnothing =\left\{a,b\right\}\right)$$
10	8 9	mtbiri	$$⊢p=\varnothing \to \neg p=\left\{a,b\right\}$$
11	10	alrimivv	$$⊢p=\varnothing \to \forall a\forall b\neg p=\left\{a,b\right\}$$
12		2nexaln	$$⊢\neg \exists a\exists bp=\left\{a,b\right\}\leftrightarrow \forall a\forall b\neg p=\left\{a,b\right\}$$
13	11 12	sylibr	$$⊢p=\varnothing \to \neg \exists a\exists bp=\left\{a,b\right\}$$
14	13	imori	$$⊢\left(\neg p=\varnothing \vee \neg \exists a\exists bp=\left\{a,b\right\}\right)$$
15	5 14	mpgbi	$$⊢\neg \exists p\left(p=\varnothing \wedge \exists a\exists bp=\left\{a,b\right\}\right)$$
16		df-nel	$$⊢\varnothing \notin \left\{p|\exists a\exists bp=\left\{a,b\right\}\right\}\leftrightarrow \neg \varnothing \in \left\{p|\exists a\exists bp=\left\{a,b\right\}\right\}$$
17		clelab	$$⊢\varnothing \in \left\{p|\exists a\exists bp=\left\{a,b\right\}\right\}\leftrightarrow \exists p\left(p=\varnothing \wedge \exists a\exists bp=\left\{a,b\right\}\right)$$
18	16 17	xchbinx	$$⊢\varnothing \notin \left\{p|\exists a\exists bp=\left\{a,b\right\}\right\}\leftrightarrow \neg \exists p\left(p=\varnothing \wedge \exists a\exists bp=\left\{a,b\right\}\right)$$
19	15 18	mpbir	$$⊢\varnothing \notin \left\{p|\exists a\exists bp=\left\{a,b\right\}\right\}$$