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