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

Theorem inundif 4484
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 3978 . . . 4 (𝑥 ∈ (𝐴𝐵) ↔ (𝑥𝐴𝑥𝐵))
2 eldif 3972 . . . 4 (𝑥 ∈ (𝐴𝐵) ↔ (𝑥𝐴 ∧ ¬ 𝑥𝐵))
31, 2orbi12i 914 . . 3 ((𝑥 ∈ (𝐴𝐵) ∨ 𝑥 ∈ (𝐴𝐵)) ↔ ((𝑥𝐴𝑥𝐵) ∨ (𝑥𝐴 ∧ ¬ 𝑥𝐵)))
4 pm4.42 1053 . . 3 (𝑥𝐴 ↔ ((𝑥𝐴𝑥𝐵) ∨ (𝑥𝐴 ∧ ¬ 𝑥𝐵)))
53, 4bitr4i 278 . 2 ((𝑥 ∈ (𝐴𝐵) ∨ 𝑥 ∈ (𝐴𝐵)) ↔ 𝑥𝐴)
65uneqri 4165 1 ((𝐴𝐵) ∪ (𝐴𝐵)) = 𝐴
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wa 395  wo 847   = wceq 1536  wcel 2105  cdif 3959  cun 3960  cin 3961
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1791  ax-4 1805  ax-5 1907  ax-6 1964  ax-7 2004  ax-8 2107  ax-9 2115  ax-ext 2705
This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-tru 1539  df-ex 1776  df-sb 2062  df-clab 2712  df-cleq 2726  df-clel 2813  df-v 3479  df-dif 3965  df-un 3967  df-in 3969
This theorem is referenced by:  iunxdif3  5099  partfun  6715  resasplit  6778  fresaun  6779  fresaunres2  6780  ixpfi2  9387  hashun3  14419  prmreclem2  16950  mvdco  19477  sylow2a  19651  ablfac1eu  20107  basdif0  22975  neitr  23203  cmpfi  23431  ptbasfi  23604  ptcnplem  23644  fin1aufil  23955  ismbl2  25575  volinun  25594  voliunlem2  25599  mbfeqalem2  25690  itg2cnlem2  25811  dvres2lem  25959  indifundif  32551  imadifxp  32620  ofpreima2  32682  resf1o  32747  gsummptres  33037  tocyccntz  33146  indsumin  34002  measun  34191  measunl  34196  inelcarsg  34292  carsgclctun  34302  sibfof  34321  probdif  34401  hgt750lemd  34641  mthmpps  35566  clcnvlem  43612  radcnvrat  44309  sumnnodd  45585  ovolsplit  45943  omelesplit  46473  ovnsplit  46603
  Copyright terms: Public domain W3C validator