Metamath Proof Explorer

Theorem uncom

Description: Commutative law for union of classes. Exercise 6 of TakeutiZaring p. 17. (Contributed by NM, 25-Jun-1998) (Proof shortened by Andrew Salmon, 26-Jun-2011)

Ref Expression
Assertion uncom A B = B A


Step Hyp Ref Expression
1 orcom x A x B x B x A
2 elun x B A x B x A
3 1 2 bitr4i x A x B x B A
4 3 uneqri A B = B A