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

Theorem undif 4001
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 3745 . 2 (𝐴𝐵 ↔ (𝐴𝐵) = 𝐵)
2 undif2 3996 . . 3 (𝐴 ∪ (𝐵𝐴)) = (𝐴𝐵)
32eqeq1i 2615 . 2 ((𝐴 ∪ (𝐵𝐴)) = 𝐵 ↔ (𝐴𝐵) = 𝐵)
41, 3bitr4i 266 1 (𝐴𝐵 ↔ (𝐴 ∪ (𝐵𝐴)) = 𝐵)
Colors of variables: wff setvar class
Syntax hints:  wb 195   = wceq 1475  cdif 3537  cun 3538  wss 3540
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590
This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-clab 2597  df-cleq 2603  df-clel 2606  df-nfc 2740  df-ral 2901  df-rab 2905  df-v 3175  df-dif 3543  df-un 3545  df-in 3547  df-ss 3554  df-nul 3875
This theorem is referenced by:  raldifeq  4011  difsnid  4282  fveqf1o  6457  ralxpmap  7793  undifixp  7830  dfdom2  7867  sbthlem5  7959  sbthlem6  7960  domunsn  7995  fodomr  7996  mapdom2  8016  limensuci  8021  findcard2  8085  unfi  8112  marypha1lem  8222  brwdom2  8361  infdifsn  8437  ackbij1lem12  8936  ackbij1lem18  8942  ssfin4  9015  fin23lem28  9045  fin23lem30  9047  fin1a2lem13  9117  canthp1lem1  9353  xrsupss  12011  xrinfmss  12012  hashssdif  13061  hashfun  13084  hashf1lem2  13097  fsumless  14369  incexclem  14407  incexc  14408  fprodsplit1f  14560  pwssplit1  18880  frlmsslss2  19933  mdetdiaglem  20223  mdetrlin  20227  mdetrsca  20228  mdetralt  20233  smadiadet  20295  isclo  20701  cmpcld  21015  rrxcph  22988  rrxdstprj1  23000  uniiccmbl  23164  itgss3  23387  dchreq  24783  axlowdimlem7  25628  axlowdimlem10  25631  padct  28885  resf1o  28893  locfinref  29236  indval2  29404  esummono  29443  gsumesum  29448  sigaclfu2  29511  measxun2  29600  measvuni  29604  measssd  29605  pmeasmono  29713  eulerpartlemt  29760  poimirlem9  32588  poimirlem15  32594  poimirlem25  32604  diophrw  36340  eldioph2lem1  36341  eldioph2lem2  36342  kelac1  36651  fsumsplit1  38639  ioccncflimc  38771  icocncflimc  38775  dirkercncflem2  38997  dirkercncflem3  38998  sge0ss  39305  meassle  39356  meadif  39372  meaiininclem  39376  isomenndlem  39420  hspmbllem1  39516  hspmbllem2  39517  ovolval4lem1  39539  fsumsplitsndif  40372
  Copyright terms: Public domain W3C validator