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	⊢ ( 𝐴 = { ∪ 𝐴 } → ∪ 𝐴 ∈ V )

Proof

Step	Hyp	Ref	Expression
1		unieq	⊢ ( 𝐴 = { ∪ 𝐴 } → ∪ 𝐴 = ∪ { ∪ 𝐴 } )
2		unieq	⊢ ( { ∪ 𝐴 } = ∅ → ∪ { ∪ 𝐴 } = ∪ ∅ )
3		uni0	⊢ ∪ ∅ = ∅
4	2 3	eqtrdi	⊢ ( { ∪ 𝐴 } = ∅ → ∪ { ∪ 𝐴 } = ∅ )
5	1 4	sylan9eq	⊢ ( ( 𝐴 = { ∪ 𝐴 } ∧ { ∪ 𝐴 } = ∅ ) → ∪ 𝐴 = ∅ )
6	5	sneqd	⊢ ( ( 𝐴 = { ∪ 𝐴 } ∧ { ∪ 𝐴 } = ∅ ) → { ∪ 𝐴 } = { ∅ } )
7		0inp0	⊢ ( { ∪ 𝐴 } = ∅ → ¬ { ∪ 𝐴 } = { ∅ } )
8	7	adantl	⊢ ( ( 𝐴 = { ∪ 𝐴 } ∧ { ∪ 𝐴 } = ∅ ) → ¬ { ∪ 𝐴 } = { ∅ } )
9	6 8	pm2.65da	⊢ ( 𝐴 = { ∪ 𝐴 } → ¬ { ∪ 𝐴 } = ∅ )
10		snprc	⊢ ( ¬ ∪ 𝐴 ∈ V ↔ { ∪ 𝐴 } = ∅ )
11	10	bicomi	⊢ ( { ∪ 𝐴 } = ∅ ↔ ¬ ∪ 𝐴 ∈ V )
12	11	con2bii	⊢ ( ∪ 𝐴 ∈ V ↔ ¬ { ∪ 𝐴 } = ∅ )
13	9 12	sylibr	⊢ ( 𝐴 = { ∪ 𝐴 } → ∪ 𝐴 ∈ V )