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

Theorem undif 3907
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 3674 . 2  |-  ( A 
C_  B  <->  ( A  u.  B )  =  B )
2 undif2 3903 . . 3  |-  ( A  u.  ( B  \  A ) )  =  ( A  u.  B
)
32eqeq1i 2474 . 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 1379    \ cdif 3473    u. cun 3474    C_ wss 3476
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1601  ax-4 1612  ax-5 1680  ax-6 1719  ax-7 1739  ax-10 1786  ax-11 1791  ax-12 1803  ax-13 1968  ax-ext 2445
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-tru 1382  df-ex 1597  df-nf 1600  df-sb 1712  df-clab 2453  df-cleq 2459  df-clel 2462  df-nfc 2617  df-ne 2664  df-ral 2819  df-rab 2823  df-v 3115  df-dif 3479  df-un 3481  df-in 3483  df-ss 3490  df-nul 3786
This theorem is referenced by:  raldifeq  3916  difsnid  4173  fveqf1o  6191  ralxpmap  7465  undifixp  7502  dfdom2  7538  sbthlem5  7628  sbthlem6  7629  domunsn  7664  fodomr  7665  mapdom2  7685  limensuci  7690  findcard2  7756  unfi  7783  marypha1lem  7889  brwdom2  7995  infdifsn  8069  cantnfrescl  8091  ackbij1lem12  8607  ackbij1lem18  8613  ssfin4  8686  fin23lem28  8716  fin23lem30  8718  fin1a2lem13  8788  canthp1lem1  9026  xrsupss  11496  xrinfmss  11497  hashssdif  12436  hashfun  12457  hashf1lem2  12467  fsumless  13569  incexclem  13607  incexc  13608  pwssplit1  17488  frlmsslss2  18572  frlmsslss2OLD  18573  mdetdiaglem  18867  mdetrlin  18871  mdetrsca  18872  mdetralt  18877  smadiadet  18939  isclo  19354  cmpcld  19668  rrxcph  21559  rrxdstprj1  21571  uniiccmbl  21734  itgss3  21956  dchreq  23261  axlowdimlem7  23927  axlowdimlem10  23930  resf1o  27225  indval2  27668  esummono  27706  gsumesum  27707  sigaclfu2  27761  measxun2  27821  measvuni  27825  measssd  27826  eulerpartlemt  27950  diophrw  30296  eldioph2lem1  30297  eldioph2lem2  30298  kelac1  30613  ioccncflimc  31224  icocncflimc  31228  dirkercncflem2  31404  dirkercncflem3  31405  fsumsplitsndif  31815
  Copyright terms: Public domain W3C validator