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

Theorem inundif 4186
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 3945 . . . 4 (𝑥 ∈ (𝐴𝐵) ↔ (𝑥𝐴𝑥𝐵))
2 eldif 3731 . . . 4 (𝑥 ∈ (𝐴𝐵) ↔ (𝑥𝐴 ∧ ¬ 𝑥𝐵))
31, 2orbi12i 879 . . 3 ((𝑥 ∈ (𝐴𝐵) ∨ 𝑥 ∈ (𝐴𝐵)) ↔ ((𝑥𝐴𝑥𝐵) ∨ (𝑥𝐴 ∧ ¬ 𝑥𝐵)))
4 pm4.42 1040 . . 3 (𝑥𝐴 ↔ ((𝑥𝐴𝑥𝐵) ∨ (𝑥𝐴 ∧ ¬ 𝑥𝐵)))
53, 4bitr4i 267 . 2 ((𝑥 ∈ (𝐴𝐵) ∨ 𝑥 ∈ (𝐴𝐵)) ↔ 𝑥𝐴)
65uneqri 3904 1 ((𝐴𝐵) ∪ (𝐴𝐵)) = 𝐴
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wa 382  wo 826   = wceq 1630  wcel 2144  cdif 3718  cun 3719  cin 3720
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1869  ax-4 1884  ax-5 1990  ax-6 2056  ax-7 2092  ax-9 2153  ax-10 2173  ax-11 2189  ax-12 2202  ax-13 2407  ax-ext 2750
This theorem depends on definitions:  df-bi 197  df-an 383  df-or 827  df-tru 1633  df-ex 1852  df-nf 1857  df-sb 2049  df-clab 2757  df-cleq 2763  df-clel 2766  df-nfc 2901  df-v 3351  df-dif 3724  df-un 3726  df-in 3728
This theorem is referenced by:  iunxdif3  4738  resasplit  6214  fresaun  6215  fresaunres2  6216  ixpfi2  8419  hashun3  13374  prmreclem2  15827  mvdco  18071  sylow2a  18240  ablfac1eu  18679  basdif0  20977  neitr  21204  cmpfi  21431  ptbasfi  21604  ptcnplem  21644  fin1aufil  21955  ismbl2  23514  volinun  23533  voliunlem2  23538  mbfeqalem  23628  itg2cnlem2  23748  dvres2lem  23893  indifundif  29688  imadifxp  29746  ofpreima2  29800  partfun  29809  resf1o  29839  gsummptres  30118  indsumin  30418  measun  30608  measunl  30613  inelcarsg  30707  carsgclctun  30717  sibfof  30736  probdif  30816  hgt750lemd  31060  mthmpps  31811  clcnvlem  38449  radcnvrat  39032  sumnnodd  40374  ovolsplit  40716  omelesplit  41246  ovnsplit  41376
  Copyright terms: Public domain W3C validator