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

Metamath Proof Explorer

Theorem unidif0OLD

Description: Obsolete version of unidif0 as of 25-Apr-2026. (Contributed by NM, 22-Mar-2004) (Proof modification is discouraged.) (New usage is discouraged.)

Ref Expression
Assertion unidif0OLD ⊢ ⋃ A ∖ ∅ = ⋃ A

Proof

Step Hyp Ref Expression
1 uniun ⊢ ⋃ A ∖ ∅ ∪ ∅ = ⋃ A ∖ ∅ ∪ ⋃ ∅
2 undif1 ⊢ A ∖ ∅ ∪ ∅ = A ∪ ∅
3 uncom ⊢ A ∪ ∅ = ∅ ∪ A
4 2 3 eqtr2i ⊢ ∅ ∪ A = A ∖ ∅ ∪ ∅
5 4 unieqi ⊢ ⋃ ∅ ∪ A = ⋃ A ∖ ∅ ∪ ∅
6 0ex ⊢ ∅ ∈ V
7 6 unisn ⊢ ⋃ ∅ = ∅
8 7 uneq2i ⊢ ⋃ A ∖ ∅ ∪ ⋃ ∅ = ⋃ A ∖ ∅ ∪ ∅
9 un0 ⊢ ⋃ A ∖ ∅ ∪ ∅ = ⋃ A ∖ ∅
10 8 9 eqtr2i ⊢ ⋃ A ∖ ∅ = ⋃ A ∖ ∅ ∪ ⋃ ∅
11 1 5 10 3eqtr4ri ⊢ ⋃ A ∖ ∅ = ⋃ ∅ ∪ A
12 uniun ⊢ ⋃ ∅ ∪ A = ⋃ ∅ ∪ ⋃ A
13 7 uneq1i ⊢ ⋃ ∅ ∪ ⋃ A = ∅ ∪ ⋃ A
14 11 12 13 3eqtri ⊢ ⋃ A ∖ ∅ = ∅ ∪ ⋃ A
15 uncom ⊢ ∅ ∪ ⋃ A = ⋃ A ∪ ∅
16 un0 ⊢ ⋃ A ∪ ∅ = ⋃ A
17 14 15 16 3eqtri ⊢ ⋃ A ∖ ∅ = ⋃ A