Theorem hashbc0

Description: The set of subsets of size zero is the singleton of the empty set. (Contributed by Mario Carneiro, 22-Apr-2015)

	Ref	Expression
Hypothesis	ramval.c	$$⊢C=\left(a\in \mathrm{V},i\in {\mathbb{N}}_0⟼\left\{b\in 𝒫a|\left|b\right|=i\right\}\right)$$
Assertion	hashbc0	$$⊢A\in V\to AC0=\left\{\varnothing \right\}$$

Proof

Step	Hyp	Ref	Expression
1		ramval.c	$$⊢C=\left(a\in \mathrm{V},i\in {\mathbb{N}}_0⟼\left\{b\in 𝒫a|\left|b\right|=i\right\}\right)$$
2		0nn0	$$⊢0\in {\mathbb{N}}_0$$
3	1	hashbcval	$$⊢\left(A\in V\wedge 0\in {\mathbb{N}}_0\right)\to AC0=\left\{x\in 𝒫A|\left|x\right|=0\right\}$$
4	2 3	mpan2	$$⊢A\in V\to AC0=\left\{x\in 𝒫A|\left|x\right|=0\right\}$$
5		hasheq0	$$⊢x\in \mathrm{V}\to \left(\left|x\right|=0\leftrightarrow x=\varnothing \right)$$
6	5	elv	$$⊢\left|x\right|=0\leftrightarrow x=\varnothing$$
7	6	anbi2i	$$⊢\left(x\in 𝒫A\wedge \left|x\right|=0\right)\leftrightarrow \left(x\in 𝒫A\wedge x=\varnothing \right)$$
8		id	$$⊢x=\varnothing \to x=\varnothing$$
9		0elpw	$$⊢\varnothing \in 𝒫A$$
10	8 9	eqeltrdi	$$⊢x=\varnothing \to x\in 𝒫A$$
11	10	pm4.71ri	$$⊢x=\varnothing \leftrightarrow \left(x\in 𝒫A\wedge x=\varnothing \right)$$
12	7 11	bitr4i	$$⊢\left(x\in 𝒫A\wedge \left|x\right|=0\right)\leftrightarrow x=\varnothing$$
13	12	abbii	$$⊢\left\{x|\left(x\in 𝒫A\wedge \left|x\right|=0\right)\right\}=\left\{x|x=\varnothing \right\}$$
14		df-rab	$$⊢\left\{x\in 𝒫A|\left|x\right|=0\right\}=\left\{x|\left(x\in 𝒫A\wedge \left|x\right|=0\right)\right\}$$
15		df-sn	$$⊢\left\{\varnothing \right\}=\left\{x|x=\varnothing \right\}$$
16	13 14 15	3eqtr4i	$$⊢\left\{x\in 𝒫A|\left|x\right|=0\right\}=\left\{\varnothing \right\}$$
17	4 16	eqtrdi	$$⊢A\in V\to AC0=\left\{\varnothing \right\}$$