Theorem eqsnuniex

Description: If a class is equal to the singleton of its union, then its union exists. (Contributed by BTernaryTau, 24-Sep-2024)

	Ref	Expression
Assertion	eqsnuniex	$$⊢A=\left\{\bigcup A\right\}\to \bigcup A\in \mathrm{V}$$

Proof

Step	Hyp	Ref	Expression
1		unieq	$$⊢A=\left\{\bigcup A\right\}\to \bigcup A=\bigcup \left\{\bigcup A\right\}$$
2		unieq	$$⊢\left\{\bigcup A\right\}=\varnothing \to \bigcup \left\{\bigcup A\right\}=\bigcup \varnothing$$
3		uni0	$$⊢\bigcup \varnothing =\varnothing$$
4	2 3	eqtrdi	$$⊢\left\{\bigcup A\right\}=\varnothing \to \bigcup \left\{\bigcup A\right\}=\varnothing$$
5	1 4	sylan9eq	$$⊢\left(A=\left\{\bigcup A\right\}\wedge \left\{\bigcup A\right\}=\varnothing \right)\to \bigcup A=\varnothing$$
6	5	sneqd	$$⊢\left(A=\left\{\bigcup A\right\}\wedge \left\{\bigcup A\right\}=\varnothing \right)\to \left\{\bigcup A\right\}=\left\{\varnothing \right\}$$
7		0inp0	$$⊢\left\{\bigcup A\right\}=\varnothing \to \neg \left\{\bigcup A\right\}=\left\{\varnothing \right\}$$
8	7	adantl	$$⊢\left(A=\left\{\bigcup A\right\}\wedge \left\{\bigcup A\right\}=\varnothing \right)\to \neg \left\{\bigcup A\right\}=\left\{\varnothing \right\}$$
9	6 8	pm2.65da	$$⊢A=\left\{\bigcup A\right\}\to \neg \left\{\bigcup A\right\}=\varnothing$$
10		snprc	$$⊢\neg \bigcup A\in \mathrm{V}\leftrightarrow \left\{\bigcup A\right\}=\varnothing$$
11	10	bicomi	$$⊢\left\{\bigcup A\right\}=\varnothing \leftrightarrow \neg \bigcup A\in \mathrm{V}$$
12	11	con2bii	$$⊢\bigcup A\in \mathrm{V}\leftrightarrow \neg \left\{\bigcup A\right\}=\varnothing$$
13	9 12	sylibr	$$⊢A=\left\{\bigcup A\right\}\to \bigcup A\in \mathrm{V}$$