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

Theorem undif 4209
Description: Union of complementary parts into whole. (Contributed by NM, 22-Mar-1998.)
Assertion
Ref Expression
undif (𝐴𝐵 ↔ (𝐴 ∪ (𝐵𝐴)) = 𝐵)

Proof of Theorem undif
StepHypRef Expression
1 ssequn1 3945 . 2 (𝐴𝐵 ↔ (𝐴𝐵) = 𝐵)
2 undif2 4204 . . 3 (𝐴 ∪ (𝐵𝐴)) = (𝐴𝐵)
32eqeq1i 2770 . 2 ((𝐴 ∪ (𝐵𝐴)) = 𝐵 ↔ (𝐴𝐵) = 𝐵)
41, 3bitr4i 269 1 (𝐴𝐵 ↔ (𝐴 ∪ (𝐵𝐴)) = 𝐵)
Colors of variables: wff setvar class
Syntax hints:  wb 197   = wceq 1652  cdif 3729  cun 3730  wss 3732
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1890  ax-4 1904  ax-5 2005  ax-6 2070  ax-7 2105  ax-9 2164  ax-10 2183  ax-11 2198  ax-12 2211  ax-13 2352  ax-ext 2743
This theorem depends on definitions:  df-bi 198  df-an 385  df-or 874  df-tru 1656  df-ex 1875  df-nf 1879  df-sb 2063  df-clab 2752  df-cleq 2758  df-clel 2761  df-nfc 2896  df-ral 3060  df-rab 3064  df-v 3352  df-dif 3735  df-un 3737  df-in 3739  df-ss 3746  df-nul 4080
This theorem is referenced by:  raldifeq  4218  difsnid  4495  fveqf1o  6749  ralxpmap  8112  undifixp  8149  dfdom2  8186  sbthlem5  8281  sbthlem6  8282  domunsn  8317  fodomr  8318  mapdom2  8338  limensuci  8343  findcard2  8407  unfi  8434  marypha1lem  8546  brwdom2  8685  infdifsn  8769  ackbij1lem12  9306  ackbij1lem18  9312  ssfin4  9385  fin23lem28  9415  fin23lem30  9417  fin1a2lem13  9487  canthp1lem1  9727  xrsupss  12341  xrinfmss  12342  hashssdif  13401  hashfun  13425  hashf1lem2  13441  fsumless  14814  incexclem  14854  incexc  14855  fprodsplit1f  15005  pwssplit1  19331  frlmsslss2  20390  mdetdiaglem  20681  mdetrlin  20685  mdetrsca  20686  mdetralt  20691  smadiadet  20754  isclo  21171  cmpcld  21485  rrxcph  23469  rrxdstprj1  23481  uniiccmbl  23648  itgss3  23872  dchreq  25274  axlowdimlem7  26119  axlowdimlem10  26122  padct  29881  resf1o  29889  fprodeq02  29953  locfinref  30290  indval2  30458  esummono  30498  gsumesum  30503  sigaclfu2  30566  measxun2  30655  measvuni  30659  measssd  30660  pmeasmono  30768  eulerpartlemt  30815  tgoldbachgtde  31121  noextendseq  32196  poimirlem9  33774  poimirlem15  33780  poimirlem25  33790  diophrw  37932  eldioph2lem1  37933  eldioph2lem2  37934  kelac1  38242  fsumsplit1  40374  ioccncflimc  40668  icocncflimc  40672  dirkercncflem2  40890  dirkercncflem3  40891  sge0ss  41198  meassle  41249  meadif  41265  meaiininclem  41272  isomenndlem  41316  hspmbllem1  41412  hspmbllem2  41413  ovolval4lem1  41435  fsumsplitsndif  42009
  Copyright terms: Public domain W3C validator