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

Theorem undif 3860
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 3616 . 2  |-  ( A 
C_  B  <->  ( A  u.  B )  =  B )
2 undif2 3855 . . 3  |-  ( A  u.  ( B  \  A ) )  =  ( A  u.  B
)
32eqeq1i 2467 . 2  |-  ( ( A  u.  ( B 
\  A ) )  =  B  <->  ( A  u.  B )  =  B )
41, 3bitr4i 260 1  |-  ( A 
C_  B  <->  ( A  u.  ( B  \  A
) )  =  B )
Colors of variables: wff setvar class
Syntax hints:    <-> wb 189    = wceq 1455    \ cdif 3413    u. cun 3414    C_ wss 3416
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1680  ax-4 1693  ax-5 1769  ax-6 1816  ax-7 1862  ax-10 1926  ax-11 1931  ax-12 1944  ax-13 2102  ax-ext 2442
This theorem depends on definitions:  df-bi 190  df-or 376  df-an 377  df-tru 1458  df-ex 1675  df-nf 1679  df-sb 1809  df-clab 2449  df-cleq 2455  df-clel 2458  df-nfc 2592  df-ne 2635  df-ral 2754  df-rab 2758  df-v 3059  df-dif 3419  df-un 3421  df-in 3423  df-ss 3430  df-nul 3744
This theorem is referenced by:  raldifeq  3869  difsnid  4131  fveqf1o  6230  ralxpmap  7552  undifixp  7589  dfdom2  7626  sbthlem5  7717  sbthlem6  7718  domunsn  7753  fodomr  7754  mapdom2  7774  limensuci  7779  findcard2  7842  unfi  7869  marypha1lem  7978  brwdom2  8119  infdifsn  8193  ackbij1lem12  8692  ackbij1lem18  8698  ssfin4  8771  fin23lem28  8801  fin23lem30  8803  fin1a2lem13  8873  canthp1lem1  9108  xrsupss  11628  xrinfmss  11629  hashssdif  12627  hashfun  12648  hashf1lem2  12658  fsumless  13911  incexclem  13949  incexc  13950  fprodsplit1f  14099  pwssplit1  18337  frlmsslss2  19388  mdetdiaglem  19678  mdetrlin  19682  mdetrsca  19683  mdetralt  19688  smadiadet  19750  isclo  20158  cmpcld  20472  rrxcph  22406  rrxdstprj1  22418  uniiccmbl  22604  itgss3  22828  dchreq  24242  axlowdimlem7  25034  axlowdimlem10  25037  padct  28359  resf1o  28367  locfinref  28719  indval2  28887  esummono  28926  gsumesum  28931  sigaclfu2  28994  measxun2  29083  measvuni  29087  measssd  29088  pmeasmono  29207  eulerpartlemt  29254  poimirlem9  31995  poimirlem15  32001  poimirlem25  32011  diophrw  35647  eldioph2lem1  35648  eldioph2lem2  35649  kelac1  35967  fsumsplit1  37736  ioccncflimc  37849  icocncflimc  37853  dirkercncflem2  38067  dirkercncflem3  38068  sge0ss  38357  meassle  38406  isomenndlem  38459  hspmbllem1  38555  hspmbllem2  38556  ovolval4lem1  38578  fsumsplitsndif  39234
  Copyright terms: Public domain W3C validator