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

Theorem inundif 4188
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 3947 . . . 4 (𝑥 ∈ (𝐴𝐵) ↔ (𝑥𝐴𝑥𝐵))
2 eldif 3733 . . . 4 (𝑥 ∈ (𝐴𝐵) ↔ (𝑥𝐴 ∧ ¬ 𝑥𝐵))
31, 2orbi12i 900 . . 3 ((𝑥 ∈ (𝐴𝐵) ∨ 𝑥 ∈ (𝐴𝐵)) ↔ ((𝑥𝐴𝑥𝐵) ∨ (𝑥𝐴 ∧ ¬ 𝑥𝐵)))
4 pm4.42 1040 . . 3 (𝑥𝐴 ↔ ((𝑥𝐴𝑥𝐵) ∨ (𝑥𝐴 ∧ ¬ 𝑥𝐵)))
53, 4bitr4i 267 . 2 ((𝑥 ∈ (𝐴𝐵) ∨ 𝑥 ∈ (𝐴𝐵)) ↔ 𝑥𝐴)
65uneqri 3906 1 ((𝐴𝐵) ∪ (𝐴𝐵)) = 𝐴
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wa 382  wo 836   = wceq 1631  wcel 2145  cdif 3720  cun 3721  cin 3722
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1870  ax-4 1885  ax-5 1991  ax-6 2057  ax-7 2093  ax-9 2154  ax-10 2174  ax-11 2190  ax-12 2203  ax-13 2408  ax-ext 2751
This theorem depends on definitions:  df-bi 197  df-an 383  df-or 837  df-tru 1634  df-ex 1853  df-nf 1858  df-sb 2050  df-clab 2758  df-cleq 2764  df-clel 2767  df-nfc 2902  df-v 3353  df-dif 3726  df-un 3728  df-in 3730
This theorem is referenced by:  iunxdif3  4740  resasplit  6212  fresaun  6213  fresaunres2  6214  ixpfi2  8418  hashun3  13368  prmreclem2  15821  mvdco  18065  sylow2a  18234  ablfac1eu  18673  basdif0  20971  neitr  21198  cmpfi  21425  ptbasfi  21598  ptcnplem  21638  fin1aufil  21949  ismbl2  23508  volinun  23527  voliunlem2  23532  mbfeqalem  23622  itg2cnlem2  23742  dvres2lem  23887  indifundif  29687  imadifxp  29745  ofpreima2  29799  partfun  29808  resf1o  29838  gsummptres  30117  indsumin  30417  measun  30607  measunl  30612  inelcarsg  30706  carsgclctun  30716  sibfof  30735  probdif  30815  hgt750lemd  31059  mthmpps  31810  clcnvlem  38449  radcnvrat  39032  sumnnodd  40373  ovolsplit  40715  omelesplit  41245  ovnsplit  41375
  Copyright terms: Public domain W3C validator