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

Theorem inundif 4479
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 3967 . . . 4 (𝑥 ∈ (𝐴𝐵) ↔ (𝑥𝐴𝑥𝐵))
2 eldif 3961 . . . 4 (𝑥 ∈ (𝐴𝐵) ↔ (𝑥𝐴 ∧ ¬ 𝑥𝐵))
31, 2orbi12i 915 . . 3 ((𝑥 ∈ (𝐴𝐵) ∨ 𝑥 ∈ (𝐴𝐵)) ↔ ((𝑥𝐴𝑥𝐵) ∨ (𝑥𝐴 ∧ ¬ 𝑥𝐵)))
4 pm4.42 1054 . . 3 (𝑥𝐴 ↔ ((𝑥𝐴𝑥𝐵) ∨ (𝑥𝐴 ∧ ¬ 𝑥𝐵)))
53, 4bitr4i 278 . 2 ((𝑥 ∈ (𝐴𝐵) ∨ 𝑥 ∈ (𝐴𝐵)) ↔ 𝑥𝐴)
65uneqri 4156 1 ((𝐴𝐵) ∪ (𝐴𝐵)) = 𝐴
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wa 395  wo 848   = wceq 1540  wcel 2108  cdif 3948  cun 3949  cin 3950
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2708
This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-tru 1543  df-ex 1780  df-sb 2065  df-clab 2715  df-cleq 2729  df-clel 2816  df-v 3482  df-dif 3954  df-un 3956  df-in 3958
This theorem is referenced by:  iunxdif3  5095  partfun  6715  resasplit  6778  fresaun  6779  fresaunres2  6780  ixpfi2  9390  hashun3  14423  prmreclem2  16955  mvdco  19463  sylow2a  19637  ablfac1eu  20093  basdif0  22960  neitr  23188  cmpfi  23416  ptbasfi  23589  ptcnplem  23629  fin1aufil  23940  ismbl2  25562  volinun  25581  voliunlem2  25586  mbfeqalem2  25677  itg2cnlem2  25797  dvres2lem  25945  indifundif  32543  imadifxp  32614  ofpreima2  32676  resf1o  32741  indsumin  32847  gsummptres  33055  tocyccntz  33164  measun  34212  measunl  34217  inelcarsg  34313  carsgclctun  34323  sibfof  34342  probdif  34422  hgt750lemd  34663  mthmpps  35587  clcnvlem  43636  radcnvrat  44333  sumnnodd  45645  ovolsplit  46003  omelesplit  46533  ovnsplit  46663
  Copyright terms: Public domain W3C validator