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

Theorem inundif 4477
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 3963 . . . 4 (𝑥 ∈ (𝐴𝐵) ↔ (𝑥𝐴𝑥𝐵))
2 eldif 3957 . . . 4 (𝑥 ∈ (𝐴𝐵) ↔ (𝑥𝐴 ∧ ¬ 𝑥𝐵))
31, 2orbi12i 911 . . 3 ((𝑥 ∈ (𝐴𝐵) ∨ 𝑥 ∈ (𝐴𝐵)) ↔ ((𝑥𝐴𝑥𝐵) ∨ (𝑥𝐴 ∧ ¬ 𝑥𝐵)))
4 pm4.42 1050 . . 3 (𝑥𝐴 ↔ ((𝑥𝐴𝑥𝐵) ∨ (𝑥𝐴 ∧ ¬ 𝑥𝐵)))
53, 4bitr4i 277 . 2 ((𝑥 ∈ (𝐴𝐵) ∨ 𝑥 ∈ (𝐴𝐵)) ↔ 𝑥𝐴)
65uneqri 4150 1 ((𝐴𝐵) ∪ (𝐴𝐵)) = 𝐴
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wa 394  wo 843   = wceq 1539  wcel 2104  cdif 3944  cun 3945  cin 3946
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1911  ax-6 1969  ax-7 2009  ax-8 2106  ax-9 2114  ax-ext 2701
This theorem depends on definitions:  df-bi 206  df-an 395  df-or 844  df-tru 1542  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2722  df-clel 2808  df-v 3474  df-dif 3950  df-un 3952  df-in 3954
This theorem is referenced by:  iunxdif3  5097  partfun  6696  resasplit  6760  fresaun  6761  fresaunres2  6762  ixpfi2  9352  hashun3  14348  prmreclem2  16854  mvdco  19354  sylow2a  19528  ablfac1eu  19984  basdif0  22676  neitr  22904  cmpfi  23132  ptbasfi  23305  ptcnplem  23345  fin1aufil  23656  ismbl2  25276  volinun  25295  voliunlem2  25300  mbfeqalem2  25391  itg2cnlem2  25512  dvres2lem  25659  indifundif  32029  imadifxp  32099  ofpreima2  32158  resf1o  32222  gsummptres  32474  tocyccntz  32573  indsumin  33318  measun  33507  measunl  33512  inelcarsg  33608  carsgclctun  33618  sibfof  33637  probdif  33717  hgt750lemd  33958  mthmpps  34871  clcnvlem  42676  radcnvrat  43375  sumnnodd  44644  ovolsplit  45002  omelesplit  45532  ovnsplit  45662
  Copyright terms: Public domain W3C validator