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

Theorem undif 4426
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 4153 . 2 (𝐴𝐵 ↔ (𝐴𝐵) = 𝐵)
2 undif2 4421 . . 3 (𝐴 ∪ (𝐵𝐴)) = (𝐴𝐵)
32eqeq1i 2823 . 2 ((𝐴 ∪ (𝐵𝐴)) = 𝐵 ↔ (𝐴𝐵) = 𝐵)
41, 3bitr4i 279 1 (𝐴𝐵 ↔ (𝐴 ∪ (𝐵𝐴)) = 𝐵)
Colors of variables: wff setvar class
Syntax hints:  wb 207   = wceq 1528  cdif 3930  cun 3931  wss 3933
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1787  ax-4 1801  ax-5 1902  ax-6 1961  ax-7 2006  ax-8 2107  ax-9 2115  ax-10 2136  ax-11 2151  ax-12 2167  ax-ext 2790
This theorem depends on definitions:  df-bi 208  df-an 397  df-or 842  df-tru 1531  df-ex 1772  df-nf 1776  df-sb 2061  df-clab 2797  df-cleq 2811  df-clel 2890  df-nfc 2960  df-rab 3144  df-v 3494  df-dif 3936  df-un 3938  df-in 3940  df-ss 3949  df-nul 4289
This theorem is referenced by:  raldifeq  4435  difsnid  4735  pwundif  5449  fveqf1o  7049  ralxpmap  8448  undifixp  8486  dfdom2  8523  sbthlem5  8619  sbthlem6  8620  domunsn  8655  fodomr  8656  mapdom2  8676  limensuci  8681  findcard2  8746  unfi  8773  marypha1lem  8885  brwdom2  9025  infdifsn  9108  ackbij1lem12  9641  ackbij1lem18  9647  ssfin4  9720  fin23lem28  9750  fin23lem30  9752  fin1a2lem13  9822  canthp1lem1  10062  xrsupss  12690  xrinfmss  12691  hashssdif  13761  hashfun  13786  hashf1lem2  13802  fsumless  15139  incexclem  15179  incexc  15180  fprodsplit1f  15332  pwssplit1  19760  frlmsslss2  20847  mdetdiaglem  21135  mdetrlin  21139  mdetrsca  21140  mdetralt  21145  smadiadet  21207  isclo  21623  cmpcld  21938  rrxcph  23922  rrxdstprj1  23939  uniiccmbl  24118  itgss3  24342  dchreq  25761  axlowdimlem7  26661  axlowdimlem10  26664  undifr  30211  padct  30381  resf1o  30392  fprodeq02  30466  cycpmcl  30685  cycpmco2  30702  cyc3co2  30709  cycpmconjslem2  30724  cyc3conja  30726  lbsdiflsp0  30921  dimkerim  30922  locfinref  31004  indval2  31172  esummono  31212  gsumesum  31217  sigaclfu2  31279  measxun2  31368  measvuni  31372  measssd  31373  pmeasmono  31481  eulerpartlemt  31528  tgoldbachgtde  31830  satfvsucsuc  32509  noextendseq  33071  poimirlem9  34782  poimirlem15  34788  poimirlem25  34798  diophrw  39234  eldioph2lem1  39235  eldioph2lem2  39236  kelac1  39541  fsumsplit1  41729  ioccncflimc  42044  icocncflimc  42048  dirkercncflem2  42266  dirkercncflem3  42267  sge0ss  42571  meassle  42622  meadif  42638  meaiininclem  42645  isomenndlem  42689  hspmbllem1  42785  hspmbllem2  42786  ovolval4lem1  42808  fsumsplitsndif  43410
  Copyright terms: Public domain W3C validator