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

Theorem inundif 4385
Description: The intersection and class difference of a class with another class unite to give the original class. (Contributed by Paul Chapman, 5-Jun-2009.) (Proof shortened by Andrew Salmon, 26-Jun-2011.)
Assertion
Ref Expression
inundif ((𝐴𝐵) ∪ (𝐴𝐵)) = 𝐴

Proof of Theorem inundif
Dummy variable 𝑥 is distinct from all other variables.
StepHypRef Expression
1 elin 3897 . . . 4 (𝑥 ∈ (𝐴𝐵) ↔ (𝑥𝐴𝑥𝐵))
2 eldif 3891 . . . 4 (𝑥 ∈ (𝐴𝐵) ↔ (𝑥𝐴 ∧ ¬ 𝑥𝐵))
31, 2orbi12i 912 . . 3 ((𝑥 ∈ (𝐴𝐵) ∨ 𝑥 ∈ (𝐴𝐵)) ↔ ((𝑥𝐴𝑥𝐵) ∨ (𝑥𝐴 ∧ ¬ 𝑥𝐵)))
4 pm4.42 1049 . . 3 (𝑥𝐴 ↔ ((𝑥𝐴𝑥𝐵) ∨ (𝑥𝐴 ∧ ¬ 𝑥𝐵)))
53, 4bitr4i 281 . 2 ((𝑥 ∈ (𝐴𝐵) ∨ 𝑥 ∈ (𝐴𝐵)) ↔ 𝑥𝐴)
65uneqri 4078 1 ((𝐴𝐵) ∪ (𝐴𝐵)) = 𝐴
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wa 399  wo 844   = wceq 1538  wcel 2111  cdif 3878  cun 3879  cin 3880
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 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-ext 2770
This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-ex 1782  df-sb 2070  df-clab 2777  df-cleq 2791  df-clel 2870  df-v 3443  df-dif 3884  df-un 3886  df-in 3888
This theorem is referenced by:  iunxdif3  4980  partfun  6467  resasplit  6522  fresaun  6523  fresaunres2  6524  ixpfi2  8806  hashun3  13741  prmreclem2  16243  mvdco  18565  sylow2a  18736  ablfac1eu  19188  basdif0  21558  neitr  21785  cmpfi  22013  ptbasfi  22186  ptcnplem  22226  fin1aufil  22537  ismbl2  24131  volinun  24150  voliunlem2  24155  mbfeqalem2  24246  itg2cnlem2  24366  dvres2lem  24513  indifundif  30297  imadifxp  30364  ofpreima2  30429  resf1o  30492  gsummptres  30737  tocyccntz  30836  indsumin  31391  measun  31580  measunl  31585  inelcarsg  31679  carsgclctun  31689  sibfof  31708  probdif  31788  hgt750lemd  32029  mthmpps  32942  clcnvlem  40321  radcnvrat  41016  sumnnodd  42270  ovolsplit  42628  omelesplit  43155  ovnsplit  43285
  Copyright terms: Public domain W3C validator