This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 )