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

Theorem inundif 4480
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 3960 . . . 4 (𝑥 ∈ (𝐴𝐵) ↔ (𝑥𝐴𝑥𝐵))
2 eldif 3954 . . . 4 (𝑥 ∈ (𝐴𝐵) ↔ (𝑥𝐴 ∧ ¬ 𝑥𝐵))
31, 2orbi12i 912 . . 3 ((𝑥 ∈ (𝐴𝐵) ∨ 𝑥 ∈ (𝐴𝐵)) ↔ ((𝑥𝐴𝑥𝐵) ∨ (𝑥𝐴 ∧ ¬ 𝑥𝐵)))
4 pm4.42 1051 . . 3 (𝑥𝐴 ↔ ((𝑥𝐴𝑥𝐵) ∨ (𝑥𝐴 ∧ ¬ 𝑥𝐵)))
53, 4bitr4i 277 . 2 ((𝑥 ∈ (𝐴𝐵) ∨ 𝑥 ∈ (𝐴𝐵)) ↔ 𝑥𝐴)
65uneqri 4148 1 ((𝐴𝐵) ∪ (𝐴𝐵)) = 𝐴
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wa 394  wo 845   = wceq 1533  wcel 2098  cdif 3941  cun 3942  cin 3943
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1905  ax-6 1963  ax-7 2003  ax-8 2100  ax-9 2108  ax-ext 2696
This theorem depends on definitions:  df-bi 206  df-an 395  df-or 846  df-tru 1536  df-ex 1774  df-sb 2060  df-clab 2703  df-cleq 2717  df-clel 2802  df-v 3463  df-dif 3947  df-un 3949  df-in 3951
This theorem is referenced by:  iunxdif3  5099  partfun  6703  resasplit  6767  fresaun  6768  fresaunres2  6769  ixpfi2  9376  hashun3  14379  prmreclem2  16889  mvdco  19412  sylow2a  19586  ablfac1eu  20042  basdif0  22900  neitr  23128  cmpfi  23356  ptbasfi  23529  ptcnplem  23569  fin1aufil  23880  ismbl2  25500  volinun  25519  voliunlem2  25524  mbfeqalem2  25615  itg2cnlem2  25736  dvres2lem  25883  indifundif  32400  imadifxp  32470  ofpreima2  32533  resf1o  32594  gsummptres  32856  tocyccntz  32957  indsumin  33772  measun  33961  measunl  33966  inelcarsg  34062  carsgclctun  34072  sibfof  34091  probdif  34171  hgt750lemd  34411  mthmpps  35323  clcnvlem  43195  radcnvrat  43893  sumnnodd  45156  ovolsplit  45514  omelesplit  46044  ovnsplit  46174
  Copyright terms: Public domain W3C validator