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

Theorem undif 3534
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 3345 . 2  |-  ( A 
C_  B  <->  ( A  u.  B )  =  B )
2 undif2 3530 . . 3  |-  ( A  u.  ( B  \  A ) )  =  ( A  u.  B
)
32eqeq1i 2290 . 2  |-  ( ( A  u.  ( B 
\  A ) )  =  B  <->  ( A  u.  B )  =  B )
41, 3bitr4i 243 1  |-  ( A 
C_  B  <->  ( A  u.  ( B  \  A
) )  =  B )
Colors of variables: wff set class
Syntax hints:    <-> wb 176    = wceq 1623    \ cdif 3149    u. cun 3150    C_ wss 3152
This theorem is referenced by:  difsnid  3761  fveqf1o  5806  undifixp  6852  dfdom2  6887  sbthlem5  6975  sbthlem6  6976  domunsn  7011  fodomr  7012  mapdom2  7032  limensuci  7037  findcard2  7098  unfi  7124  marypha1lem  7186  brwdom2  7287  infdifsn  7357  cantnfrescl  7378  ackbij1lem12  7857  ackbij1lem18  7863  ssfin4  7936  fin23lem28  7966  fin23lem30  7968  fin1a2lem13  8038  canthp1lem1  8274  xrsupss  10627  xrinfmss  10628  hashssdif  11374  hashfun  11389  hashf1lem2  11394  fsumless  12254  incexclem  12295  incexc  12296  isclo  16824  cmpcld  17129  uniiccmbl  18945  itgss3  19169  dchreq  20497  sigaclfu2  23482  measxun2  23538  measvuni  23542  measssd  23543  indval2  23598  axlowdimlem7  24576  axlowdimlem10  24579  splint  25048  ralxpmap  26761  diophrw  26838  eldioph2lem1  26839  eldioph2lem2  26840  kelac1  27161  pwssplit1  27188  frlmsslss2  27245
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1533  ax-5 1544  ax-17 1603  ax-9 1635  ax-8 1643  ax-6 1703  ax-7 1708  ax-11 1715  ax-12 1866  ax-ext 2264
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-tru 1310  df-ex 1529  df-nf 1532  df-sb 1630  df-clab 2270  df-cleq 2276  df-clel 2279  df-nfc 2408  df-ne 2448  df-ral 2548  df-rab 2552  df-v 2790  df-dif 3155  df-un 3157  df-in 3159  df-ss 3166  df-nul 3456
  Copyright terms: Public domain W3C validator