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 = { U. A } -> U. A e. _V )

Proof

Step	Hyp	Ref	Expression
1		unieq	|- ( A = { U. A } -> U. A = U. { U. A } )
2		unieq	|- ( { U. A } = (/) -> U. { U. A } = U. (/) )
3		uni0	|- U. (/) = (/)
4	2 3	eqtrdi	|- ( { U. A } = (/) -> U. { U. A } = (/) )
5	1 4	sylan9eq	|- ( ( A = { U. A } /\ { U. A } = (/) ) -> U. A = (/) )
6	5	sneqd	|- ( ( A = { U. A } /\ { U. A } = (/) ) -> { U. A } = { (/) } )
7		0inp0	|- ( { U. A } = (/) -> -. { U. A } = { (/) } )
8	7	adantl	|- ( ( A = { U. A } /\ { U. A } = (/) ) -> -. { U. A } = { (/) } )
9	6 8	pm2.65da	|- ( A = { U. A } -> -. { U. A } = (/) )
10		snprc	|- ( -. U. A e. _V <-> { U. A } = (/) )
11	10	bicomi	|- ( { U. A } = (/) <-> -. U. A e. _V )
12	11	con2bii	|- ( U. A e. _V <-> -. { U. A } = (/) )
13	9 12	sylibr	|- ( A = { U. A } -> U. A e. _V )