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

Theorem inundif 4044
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 3794 . . . 4 (𝑥 ∈ (𝐴𝐵) ↔ (𝑥𝐴𝑥𝐵))
2 eldif 3582 . . . 4 (𝑥 ∈ (𝐴𝐵) ↔ (𝑥𝐴 ∧ ¬ 𝑥𝐵))
31, 2orbi12i 543 . . 3 ((𝑥 ∈ (𝐴𝐵) ∨ 𝑥 ∈ (𝐴𝐵)) ↔ ((𝑥𝐴𝑥𝐵) ∨ (𝑥𝐴 ∧ ¬ 𝑥𝐵)))
4 pm4.42 1004 . . 3 (𝑥𝐴 ↔ ((𝑥𝐴𝑥𝐵) ∨ (𝑥𝐴 ∧ ¬ 𝑥𝐵)))
53, 4bitr4i 267 . 2 ((𝑥 ∈ (𝐴𝐵) ∨ 𝑥 ∈ (𝐴𝐵)) ↔ 𝑥𝐴)
65uneqri 3753 1 ((𝐴𝐵) ∪ (𝐴𝐵)) = 𝐴
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wo 383  wa 384   = wceq 1482  wcel 1989  cdif 3569  cun 3570  cin 3571
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1721  ax-4 1736  ax-5 1838  ax-6 1887  ax-7 1934  ax-9 1998  ax-10 2018  ax-11 2033  ax-12 2046  ax-13 2245  ax-ext 2601
This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-tru 1485  df-ex 1704  df-nf 1709  df-sb 1880  df-clab 2608  df-cleq 2614  df-clel 2617  df-nfc 2752  df-v 3200  df-dif 3575  df-un 3577  df-in 3579
This theorem is referenced by:  iunxdif3  4604  resasplit  6072  fresaun  6073  fresaunres2  6074  ixpfi2  8261  hashun3  13168  prmreclem2  15615  mvdco  17859  sylow2a  18028  ablfac1eu  18466  basdif0  20751  neitr  20978  cmpfi  21205  ptbasfi  21378  ptcnplem  21418  fin1aufil  21730  ismbl2  23289  volinun  23308  voliunlem2  23313  mbfeqalem  23403  itg2cnlem2  23523  dvres2lem  23668  indifundif  29340  imadifxp  29398  ofpreima2  29451  partfun  29460  resf1o  29490  gsummptres  29769  indsumin  30069  measun  30259  measunl  30264  inelcarsg  30358  carsgclctun  30368  sibfof  30387  probdif  30467  hgt750lemd  30711  mthmpps  31464  clcnvlem  37756  radcnvrat  38339  sumnnodd  39668  ovolsplit  39974  omelesplit  40501  ovnsplit  40631
  Copyright terms: Public domain W3C validator