Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  unass Structured version   Visualization version   GIF version

Theorem unass 4128
 Description: Associative law for union of classes. Exercise 8 of [TakeutiZaring] p. 17. (Contributed by NM, 3-May-1994.) (Proof shortened by Andrew Salmon, 26-Jun-2011.)
Assertion
Ref Expression
unass ((𝐴𝐵) ∪ 𝐶) = (𝐴 ∪ (𝐵𝐶))

Proof of Theorem unass
Dummy variable 𝑥 is distinct from all other variables.
StepHypRef Expression
1 elun 4111 . . 3 (𝑥 ∈ (𝐴 ∪ (𝐵𝐶)) ↔ (𝑥𝐴𝑥 ∈ (𝐵𝐶)))
2 elun 4111 . . . 4 (𝑥 ∈ (𝐵𝐶) ↔ (𝑥𝐵𝑥𝐶))
32orbi2i 910 . . 3 ((𝑥𝐴𝑥 ∈ (𝐵𝐶)) ↔ (𝑥𝐴 ∨ (𝑥𝐵𝑥𝐶)))
4 elun 4111 . . . . 5 (𝑥 ∈ (𝐴𝐵) ↔ (𝑥𝐴𝑥𝐵))
54orbi1i 911 . . . 4 ((𝑥 ∈ (𝐴𝐵) ∨ 𝑥𝐶) ↔ ((𝑥𝐴𝑥𝐵) ∨ 𝑥𝐶))
6 orass 919 . . . 4 (((𝑥𝐴𝑥𝐵) ∨ 𝑥𝐶) ↔ (𝑥𝐴 ∨ (𝑥𝐵𝑥𝐶)))
75, 6bitr2i 279 . . 3 ((𝑥𝐴 ∨ (𝑥𝐵𝑥𝐶)) ↔ (𝑥 ∈ (𝐴𝐵) ∨ 𝑥𝐶))
81, 3, 73bitrri 301 . 2 ((𝑥 ∈ (𝐴𝐵) ∨ 𝑥𝐶) ↔ 𝑥 ∈ (𝐴 ∪ (𝐵𝐶)))
98uneqri 4113 1 ((𝐴𝐵) ∪ 𝐶) = (𝐴 ∪ (𝐵𝐶))
 Colors of variables: wff setvar class Syntax hints:   ∨ wo 844   = wceq 1538   ∈ wcel 2115   ∪ cun 3917 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1971  ax-7 2016  ax-8 2117  ax-9 2125  ax-ext 2796 This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-ex 1782  df-sb 2071  df-clab 2803  df-cleq 2817  df-clel 2896  df-v 3482  df-un 3924 This theorem is referenced by:  un12  4129  un23  4130  un4  4131  dfif5  4466  qdass  4674  qdassr  4675  ssunpr  4749  oarec  8186  domunfican  8790  djuassen  9604  prunioo  12870  ioojoin  12872  fzosplitpr  13152  s4prop  14274  lcmfun  15989  phlstr  16655  prdsvalstr  16728  mreexexlem2d  16918  mreexexlem4d  16920  pwmnd  18104  ordtbas  21806  reconnlem1  23440  lhop  24628  plyun0  24803  ex-un  28218  ex-pw  28223  indifundif  30303  subfacp1lem1  32511  poimirlem3  35032  poimirlem4  35033  poimirlem16  35045  poimirlem19  35048  dfrcl2  40319  corcltrcl  40384  cotrclrcl  40387  frege131d  40409
 Copyright terms: Public domain W3C validator