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 3965 . . . 4 (𝑥 ∈ (𝐴𝐵) ↔ (𝑥𝐴𝑥𝐵))
2 eldif 3959 . . . 4 (𝑥 ∈ (𝐴𝐵) ↔ (𝑥𝐴 ∧ ¬ 𝑥𝐵))
31, 2orbi12i 914 . . 3 ((𝑥 ∈ (𝐴𝐵) ∨ 𝑥 ∈ (𝐴𝐵)) ↔ ((𝑥𝐴𝑥𝐵) ∨ (𝑥𝐴 ∧ ¬ 𝑥𝐵)))
4 pm4.42 1053 . . 3 (𝑥𝐴 ↔ ((𝑥𝐴𝑥𝐵) ∨ (𝑥𝐴 ∧ ¬ 𝑥𝐵)))
53, 4bitr4i 278 . 2 ((𝑥 ∈ (𝐴𝐵) ∨ 𝑥 ∈ (𝐴𝐵)) ↔ 𝑥𝐴)
65uneqri 4152 1 ((𝐴𝐵) ∪ (𝐴𝐵)) = 𝐴
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wa 397  wo 846   = wceq 1542  wcel 2107  cdif 3946  cun 3947  cin 3948
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2704
This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-tru 1545  df-ex 1783  df-sb 2069  df-clab 2711  df-cleq 2725  df-clel 2811  df-v 3477  df-dif 3952  df-un 3954  df-in 3956
This theorem is referenced by:  iunxdif3  5099  partfun  6698  resasplit  6762  fresaun  6763  fresaunres2  6764  ixpfi2  9350  hashun3  14344  prmreclem2  16850  mvdco  19313  sylow2a  19487  ablfac1eu  19943  basdif0  22456  neitr  22684  cmpfi  22912  ptbasfi  23085  ptcnplem  23125  fin1aufil  23436  ismbl2  25044  volinun  25063  voliunlem2  25068  mbfeqalem2  25159  itg2cnlem2  25280  dvres2lem  25427  indifundif  31762  imadifxp  31832  ofpreima2  31891  resf1o  31955  gsummptres  32204  tocyccntz  32303  indsumin  33020  measun  33209  measunl  33214  inelcarsg  33310  carsgclctun  33320  sibfof  33339  probdif  33419  hgt750lemd  33660  mthmpps  34573  clcnvlem  42374  radcnvrat  43073  sumnnodd  44346  ovolsplit  44704  omelesplit  45234  ovnsplit  45364
  Copyright terms: Public domain W3C validator