Theorem unisnif

Description: Express union of singleton in terms of if . (Contributed by Scott Fenton, 27-Mar-2014) (Revised by Mario Carneiro, 19-Apr-2014)

	Ref	Expression
Assertion	unisnif	$$⊢\bigcup \left\{A\right\}=if\left(A\in \mathrm{V},A,\varnothing \right)$$

Proof

Step	Hyp	Ref	Expression
1		iftrue	$$⊢A\in \mathrm{V}\to if\left(A\in \mathrm{V},A,\varnothing \right)=A$$
2		unisng	$$⊢A\in \mathrm{V}\to \bigcup \left\{A\right\}=A$$
3	1 2	eqtr4d	$$⊢A\in \mathrm{V}\to if\left(A\in \mathrm{V},A,\varnothing \right)=\bigcup \left\{A\right\}$$
4		iffalse	$$⊢\neg A\in \mathrm{V}\to if\left(A\in \mathrm{V},A,\varnothing \right)=\varnothing$$
5		snprc	$$⊢\neg A\in \mathrm{V}\leftrightarrow \left\{A\right\}=\varnothing$$
6	5	biimpi	$$⊢\neg A\in \mathrm{V}\to \left\{A\right\}=\varnothing$$
7	6	unieqd	$$⊢\neg A\in \mathrm{V}\to \bigcup \left\{A\right\}=\bigcup \varnothing$$
8		uni0	$$⊢\bigcup \varnothing =\varnothing$$
9	7 8	eqtrdi	$$⊢\neg A\in \mathrm{V}\to \bigcup \left\{A\right\}=\varnothing$$
10	4 9	eqtr4d	$$⊢\neg A\in \mathrm{V}\to if\left(A\in \mathrm{V},A,\varnothing \right)=\bigcup \left\{A\right\}$$
11	3 10	pm2.61i	$$⊢if\left(A\in \mathrm{V},A,\varnothing \right)=\bigcup \left\{A\right\}$$
12	11	eqcomi	$$⊢\bigcup \left\{A\right\}=if\left(A\in \mathrm{V},A,\varnothing \right)$$