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