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

Theorem undif 3894
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 3659 . 2  |-  ( A 
C_  B  <->  ( A  u.  B )  =  B )
2 undif2 3890 . . 3  |-  ( A  u.  ( B  \  A ) )  =  ( A  u.  B
)
32eqeq1i 2450 . 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 1383    \ cdif 3458    u. cun 3459    C_ wss 3461
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1605  ax-4 1618  ax-5 1691  ax-6 1734  ax-7 1776  ax-10 1823  ax-11 1828  ax-12 1840  ax-13 1985  ax-ext 2421
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-tru 1386  df-ex 1600  df-nf 1604  df-sb 1727  df-clab 2429  df-cleq 2435  df-clel 2438  df-nfc 2593  df-ne 2640  df-ral 2798  df-rab 2802  df-v 3097  df-dif 3464  df-un 3466  df-in 3468  df-ss 3475  df-nul 3771
This theorem is referenced by:  raldifeq  3903  difsnid  4161  fveqf1o  6190  ralxpmap  7470  undifixp  7507  dfdom2  7543  sbthlem5  7633  sbthlem6  7634  domunsn  7669  fodomr  7670  mapdom2  7690  limensuci  7695  findcard2  7762  unfi  7789  marypha1lem  7895  brwdom2  8002  infdifsn  8076  ackbij1lem12  8614  ackbij1lem18  8620  ssfin4  8693  fin23lem28  8723  fin23lem30  8725  fin1a2lem13  8795  canthp1lem1  9033  xrsupss  11511  xrinfmss  11512  hashssdif  12457  hashfun  12477  hashf1lem2  12487  fsumless  13592  incexclem  13630  incexc  13631  pwssplit1  17684  frlmsslss2  18783  frlmsslss2OLD  18784  mdetdiaglem  19078  mdetrlin  19082  mdetrsca  19083  mdetralt  19088  smadiadet  19150  isclo  19566  cmpcld  19880  rrxcph  21802  rrxdstprj1  21814  uniiccmbl  21977  itgss3  22199  dchreq  23511  axlowdimlem7  24229  axlowdimlem10  24232  resf1o  27531  locfinref  27822  indval2  28006  esummono  28044  gsumesum  28045  sigaclfu2  28099  measxun2  28159  measvuni  28163  measssd  28164  eulerpartlemt  28288  diophrw  30668  eldioph2lem1  30669  eldioph2lem2  30670  kelac1  30985  fsumsplit1  31527  fprodsplit1f  31547  ioccncflimc  31642  icocncflimc  31646  dirkercncflem2  31840  dirkercncflem3  31841  fsumsplitsndif  32300
  Copyright terms: Public domain W3C validator