Theorem uncom 2176

Description: Commutative law for union of classes. Exercise 6 of [TakeutiZaring] p. 17.

Assertion

Ref	Expression
uncom	|- (A u. B) = (B u. A)

Proof of Theorem uncom

Step	Hyp	Ref	Expression
1		orcom 246	. . 3 |- ((x e. A \/ x e. B) <-> (x e. B \/ x e. A))
2		elun 2173	. . 3 |- (x e. (A u. B) <-> (x e. A \/ x e. B))
3		elun 2173	. . 3 |- (x e. (B u. A) <-> (x e. B \/ x e. A))
4	1, 2, 3	3bitr4 183	. 2 |- (x e. (A u. B) <-> x e. (B u. A))
5	4	eqriv 1474	1 |- (A u. B) = (B u. A)

Syntax hints:   \/ wo 222   = wceq 956   e. wcel 958   u. cun 2045

This theorem is referenced by:  uneq2 2178  un12 2188  un23 2189  ssun2 2194  unss2 2201  ssequn2 2203  undir 2254  unineq 2255  dif23 2264  disjpss 2319  undif1 2340  undif2 2341  difcom 2345  prcom 2447  prprc1 2452  difsnid 2467  unidif0 2739  elpwun 2911  suc0 3043  unidmrn 3516  fvsnun2 3796  oev2 4162  dfdom2 4384  mapunen 4502  limensuci 4506  phplem1 4508  phplem2 4509  cdacomen 4929  ssxr 5540  xrsupss 6078  xrinfmss 6079  supxrmnf 6087  dfisum 7191  acdc2lem2 7489  acdc5lem2 7492  ruclem6 7515  infcda 7567  infxp 7572  alephadd 7582  indistop 7648  indistps 7653  shjcomt 9330  mapudiscn 10512  eqindhome 10541

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 962  ax-gen 963  ax-8 964  ax-10 966  ax-12 968  ax-17 971  ax-4 973  ax-5o 975  ax-6o 978  ax-9o 1123  ax-10o 1140  ax-16 1210  ax-11o 1218  ax-ext 1459

This theorem depends on definitions:  df-bi 147  df-or 224  df-an 225  df-ex 981  df-sb 1172  df-clab 1464  df-cleq 1469  df-clel 1472  df-v 1812  df-un 2050

Copyright terms: Public domain