Theorem unisn2

Description: A version of unisn without the A e. _V hypothesis. (Contributed by Stefan Allan, 14-Mar-2006)

	Ref	Expression
Assertion	unisn2	$$⊢\bigcup \left\{A\right\}\in \left\{\varnothing ,A\right\}$$

Proof

Step	Hyp	Ref	Expression
1		unisng	$$⊢A\in \mathrm{V}\to \bigcup \left\{A\right\}=A$$
2		prid2g	$$⊢A\in \mathrm{V}\to A\in \left\{\varnothing ,A\right\}$$
3	1 2	eqeltrd	$$⊢A\in \mathrm{V}\to \bigcup \left\{A\right\}\in \left\{\varnothing ,A\right\}$$
4		snprc	$$⊢\neg A\in \mathrm{V}\leftrightarrow \left\{A\right\}=\varnothing$$
5	4	biimpi	$$⊢\neg A\in \mathrm{V}\to \left\{A\right\}=\varnothing$$
6	5	unieqd	$$⊢\neg A\in \mathrm{V}\to \bigcup \left\{A\right\}=\bigcup \varnothing$$
7		uni0	$$⊢\bigcup \varnothing =\varnothing$$
8		0ex	$$⊢\varnothing \in \mathrm{V}$$
9	8	prid1	$$⊢\varnothing \in \left\{\varnothing ,A\right\}$$
10	7 9	eqeltri	$$⊢\bigcup \varnothing \in \left\{\varnothing ,A\right\}$$
11	6 10	eqeltrdi	$$⊢\neg A\in \mathrm{V}\to \bigcup \left\{A\right\}\in \left\{\varnothing ,A\right\}$$
12	3 11	pm2.61i	$$⊢\bigcup \left\{A\right\}\in \left\{\varnothing ,A\right\}$$