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

Theorem undif 3762
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 3529 . 2  |-  ( A 
C_  B  <->  ( A  u.  B )  =  B )
2 undif2 3758 . . 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 1369    \ cdif 3328    u. cun 3329    C_ wss 3331
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-10 1775  ax-11 1780  ax-12 1792  ax-13 1943  ax-ext 2423
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-tru 1372  df-ex 1587  df-nf 1590  df-sb 1701  df-clab 2430  df-cleq 2436  df-clel 2439  df-nfc 2571  df-ne 2611  df-ral 2723  df-rab 2727  df-v 2977  df-dif 3334  df-un 3336  df-in 3338  df-ss 3345  df-nul 3641
This theorem is referenced by:  raldifeq  3771  difsnid  4022  fveqf1o  6003  ralxpmap  7265  undifixp  7302  dfdom2  7338  sbthlem5  7428  sbthlem6  7429  domunsn  7464  fodomr  7465  mapdom2  7485  limensuci  7490  findcard2  7555  unfi  7582  marypha1lem  7686  brwdom2  7791  infdifsn  7865  cantnfrescl  7887  ackbij1lem12  8403  ackbij1lem18  8409  ssfin4  8482  fin23lem28  8512  fin23lem30  8514  fin1a2lem13  8584  canthp1lem1  8822  xrsupss  11274  xrinfmss  11275  hashssdif  12170  hashfun  12202  hashf1lem2  12212  fsumless  13262  incexclem  13302  incexc  13303  pwssplit1  17143  frlmsslss2  18202  frlmsslss2OLD  18203  mdet1  18411  mdetrlin  18412  mdetrsca  18413  mdetralt  18417  smadiadet  18479  isclo  18694  cmpcld  19008  rrxcph  20899  rrxdstprj1  20911  uniiccmbl  21073  itgss3  21295  dchreq  22600  axlowdimlem7  23197  axlowdimlem10  23200  resf1o  26033  indval2  26474  esummono  26512  gsumesum  26513  sigaclfu2  26567  measxun2  26627  measvuni  26631  measssd  26632  eulerpartlemt  26757  diophrw  29100  eldioph2lem1  29101  eldioph2lem2  29102  kelac1  29419  fsumsplitsndif  30241  mdetdiaglem  30938
  Copyright terms: Public domain W3C validator