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

Theorem undif 3747
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 3514 . 2  |-  ( A 
C_  B  <->  ( A  u.  B )  =  B )
2 undif2 3743 . . 3  |-  ( A  u.  ( B  \  A ) )  =  ( A  u.  B
)
32eqeq1i 2440 . 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 1362    \ cdif 3313    u. cun 3314    C_ wss 3316
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1594  ax-4 1605  ax-5 1669  ax-6 1707  ax-7 1727  ax-10 1774  ax-11 1779  ax-12 1791  ax-13 1942  ax-ext 2414
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-tru 1365  df-ex 1590  df-nf 1593  df-sb 1700  df-clab 2420  df-cleq 2426  df-clel 2429  df-nfc 2558  df-ne 2598  df-ral 2710  df-rab 2714  df-v 2964  df-dif 3319  df-un 3321  df-in 3323  df-ss 3330  df-nul 3626
This theorem is referenced by:  raldifeq  3756  difsnid  4007  fveqf1o  5987  ralxpmap  7250  undifixp  7287  dfdom2  7323  sbthlem5  7413  sbthlem6  7414  domunsn  7449  fodomr  7450  mapdom2  7470  limensuci  7475  findcard2  7540  unfi  7567  marypha1lem  7671  brwdom2  7776  infdifsn  7850  cantnfrescl  7872  ackbij1lem12  8388  ackbij1lem18  8394  ssfin4  8467  fin23lem28  8497  fin23lem30  8499  fin1a2lem13  8569  canthp1lem1  8807  xrsupss  11259  xrinfmss  11260  hashssdif  12151  hashfun  12183  hashf1lem2  12193  fsumless  13242  incexclem  13282  incexc  13283  pwssplit1  17062  frlmsslss2  18041  frlmsslss2OLD  18042  mdet1  18250  mdetrlin  18251  mdetrsca  18252  mdetralt  18256  smadiadet  18318  isclo  18533  cmpcld  18847  rrxcph  20738  rrxdstprj1  20750  uniiccmbl  20912  itgss3  21134  dchreq  22482  axlowdimlem7  23017  axlowdimlem10  23020  resf1o  25855  indval2  26325  esummono  26363  gsumesum  26364  sigaclfu2  26418  measxun2  26478  measvuni  26482  measssd  26483  eulerpartlemt  26602  diophrw  28942  eldioph2lem1  28943  eldioph2lem2  28944  kelac1  29261  fsumsplitsndif  30084  mdetdiaglem  30665
  Copyright terms: Public domain W3C validator