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

Theorem inundif 4304
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 4053 . . . 4 (𝑥 ∈ (𝐴𝐵) ↔ (𝑥𝐴𝑥𝐵))
2 eldif 3835 . . . 4 (𝑥 ∈ (𝐴𝐵) ↔ (𝑥𝐴 ∧ ¬ 𝑥𝐵))
31, 2orbi12i 898 . . 3 ((𝑥 ∈ (𝐴𝐵) ∨ 𝑥 ∈ (𝐴𝐵)) ↔ ((𝑥𝐴𝑥𝐵) ∨ (𝑥𝐴 ∧ ¬ 𝑥𝐵)))
4 pm4.42 1034 . . 3 (𝑥𝐴 ↔ ((𝑥𝐴𝑥𝐵) ∨ (𝑥𝐴 ∧ ¬ 𝑥𝐵)))
53, 4bitr4i 270 . 2 ((𝑥 ∈ (𝐴𝐵) ∨ 𝑥 ∈ (𝐴𝐵)) ↔ 𝑥𝐴)
65uneqri 4012 1 ((𝐴𝐵) ∪ (𝐴𝐵)) = 𝐴
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wa 387  wo 833   = wceq 1507  wcel 2048  cdif 3822  cun 3823  cin 3824
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1758  ax-4 1772  ax-5 1869  ax-6 1928  ax-7 1964  ax-8 2050  ax-9 2057  ax-10 2077  ax-11 2091  ax-12 2104  ax-ext 2745
This theorem depends on definitions:  df-bi 199  df-an 388  df-or 834  df-tru 1510  df-ex 1743  df-nf 1747  df-sb 2014  df-clab 2754  df-cleq 2765  df-clel 2840  df-nfc 2912  df-v 3411  df-dif 3828  df-un 3830  df-in 3832
This theorem is referenced by:  iunxdif3  4877  resasplit  6371  fresaun  6372  fresaunres2  6373  ixpfi2  8609  hashun3  13551  prmreclem2  16099  mvdco  18324  sylow2a  18495  ablfac1eu  18935  basdif0  21255  neitr  21482  cmpfi  21710  ptbasfi  21883  ptcnplem  21923  fin1aufil  22234  ismbl2  23821  volinun  23840  voliunlem2  23845  mbfeqalem2  23936  itg2cnlem2  24056  dvres2lem  24201  indifundif  30049  imadifxp  30107  ofpreima2  30163  partfun  30173  resf1o  30207  gsummptres  30485  indsumin  30882  measun  31072  measunl  31077  inelcarsg  31171  carsgclctun  31181  sibfof  31200  probdif  31281  hgt750lemd  31528  mthmpps  32289  clcnvlem  39291  radcnvrat  40006  sumnnodd  41288  ovolsplit  41650  omelesplit  42177  ovnsplit  42307
  Copyright terms: Public domain W3C validator