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

Theorem undif 3849
Description: Union of complementary parts into whole. (Contributed by NM, 22-Mar-1998.)
Assertion
Ref Expression
undif  |-  ( A 
C_  B  <->  ( A  u.  ( B  \  A
) )  =  B )

Proof of Theorem undif
StepHypRef Expression
1 ssequn1 3610 . 2  |-  ( A 
C_  B  <->  ( A  u.  B )  =  B )
2 undif2 3845 . . 3  |-  ( A  u.  ( B  \  A ) )  =  ( A  u.  B
)
32eqeq1i 2407 . 2  |-  ( ( A  u.  ( B 
\  A ) )  =  B  <->  ( A  u.  B )  =  B )
41, 3bitr4i 252 1  |-  ( A 
C_  B  <->  ( A  u.  ( B  \  A
) )  =  B )
Colors of variables: wff setvar class
Syntax hints:    <-> wb 184    = wceq 1403    \ cdif 3408    u. cun 3409    C_ wss 3411
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1637  ax-4 1650  ax-5 1723  ax-6 1769  ax-7 1812  ax-10 1859  ax-11 1864  ax-12 1876  ax-13 2024  ax-ext 2378
This theorem depends on definitions:  df-bi 185  df-or 368  df-an 369  df-tru 1406  df-ex 1632  df-nf 1636  df-sb 1762  df-clab 2386  df-cleq 2392  df-clel 2395  df-nfc 2550  df-ne 2598  df-ral 2756  df-rab 2760  df-v 3058  df-dif 3414  df-un 3416  df-in 3418  df-ss 3425  df-nul 3736
This theorem is referenced by:  raldifeq  3858  difsnid  4115  fveqf1o  6142  ralxpmap  7424  undifixp  7461  dfdom2  7497  sbthlem5  7587  sbthlem6  7588  domunsn  7623  fodomr  7624  mapdom2  7644  limensuci  7649  findcard2  7712  unfi  7739  marypha1lem  7845  brwdom2  7951  infdifsn  8024  ackbij1lem12  8561  ackbij1lem18  8567  ssfin4  8640  fin23lem28  8670  fin23lem30  8672  fin1a2lem13  8742  canthp1lem1  8978  xrsupss  11469  xrinfmss  11470  hashssdif  12429  hashfun  12449  hashf1lem2  12459  fsumless  13666  incexclem  13704  incexc  13705  pwssplit1  17915  frlmsslss2  18991  frlmsslss2OLD  18992  mdetdiaglem  19282  mdetrlin  19286  mdetrsca  19287  mdetralt  19292  smadiadet  19354  isclo  19771  cmpcld  20085  rrxcph  22006  rrxdstprj1  22018  uniiccmbl  22181  itgss3  22403  dchreq  23804  axlowdimlem7  24550  axlowdimlem10  24553  padct  27873  resf1o  27881  locfinref  28178  indval2  28343  esummono  28382  gsumesum  28387  sigaclfu2  28450  measxun2  28539  measvuni  28543  measssd  28544  pmeasmono  28653  eulerpartlemt  28697  diophrw  35017  eldioph2lem1  35018  eldioph2lem2  35019  kelac1  35335  fsumsplit1  36908  fprodsplit1f  36928  ioccncflimc  37023  icocncflimc  37027  dirkercncflem2  37221  dirkercncflem3  37222  fsumsplitsndif  37908
  Copyright terms: Public domain W3C validator