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 = \{⋃ A\} \to ⋃ A \in V$

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

Metamath Proof Explorer