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

Theorem inundif 4439
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 3927 . . . 4 (𝑥 ∈ (𝐴𝐵) ↔ (𝑥𝐴𝑥𝐵))
2 eldif 3921 . . . 4 (𝑥 ∈ (𝐴𝐵) ↔ (𝑥𝐴 ∧ ¬ 𝑥𝐵))
31, 2orbi12i 914 . . 3 ((𝑥 ∈ (𝐴𝐵) ∨ 𝑥 ∈ (𝐴𝐵)) ↔ ((𝑥𝐴𝑥𝐵) ∨ (𝑥𝐴 ∧ ¬ 𝑥𝐵)))
4 pm4.42 1053 . . 3 (𝑥𝐴 ↔ ((𝑥𝐴𝑥𝐵) ∨ (𝑥𝐴 ∧ ¬ 𝑥𝐵)))
53, 4bitr4i 278 . 2 ((𝑥 ∈ (𝐴𝐵) ∨ 𝑥 ∈ (𝐴𝐵)) ↔ 𝑥𝐴)
65uneqri 4112 1 ((𝐴𝐵) ∪ (𝐴𝐵)) = 𝐴
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wa 397  wo 846   = wceq 1542  wcel 2107  cdif 3908  cun 3909  cin 3910
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2708
This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-tru 1545  df-ex 1783  df-sb 2069  df-clab 2715  df-cleq 2729  df-clel 2815  df-v 3448  df-dif 3914  df-un 3916  df-in 3918
This theorem is referenced by:  iunxdif3  5056  partfun  6649  resasplit  6713  fresaun  6714  fresaunres2  6715  ixpfi2  9295  hashun3  14285  prmreclem2  16790  mvdco  19228  sylow2a  19402  ablfac1eu  19853  basdif0  22306  neitr  22534  cmpfi  22762  ptbasfi  22935  ptcnplem  22975  fin1aufil  23286  ismbl2  24894  volinun  24913  voliunlem2  24918  mbfeqalem2  25009  itg2cnlem2  25130  dvres2lem  25277  indifundif  31455  imadifxp  31522  ofpreima2  31585  resf1o  31650  gsummptres  31897  tocyccntz  31996  indsumin  32624  measun  32813  measunl  32818  inelcarsg  32914  carsgclctun  32924  sibfof  32943  probdif  33023  hgt750lemd  33264  mthmpps  34179  clcnvlem  41902  radcnvrat  42601  sumnnodd  43878  ovolsplit  44236  omelesplit  44766  ovnsplit  44896
  Copyright terms: Public domain W3C validator