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

Theorem undif 3700
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 3509 . 2  |-  ( A 
C_  B  <->  ( A  u.  B )  =  B )
2 undif2 3696 . . 3  |-  ( A  u.  ( B  \  A ) )  =  ( A  u.  B
)
32eqeq1i 2442 . 2  |-  ( ( A  u.  ( B 
\  A ) )  =  B  <->  ( A  u.  B )  =  B )
41, 3bitr4i 244 1  |-  ( A 
C_  B  <->  ( A  u.  ( B  \  A
) )  =  B )
Colors of variables: wff set class
Syntax hints:    <-> wb 177    = wceq 1652    \ cdif 3309    u. cun 3310    C_ wss 3312
This theorem is referenced by:  difsnid  3936  fveqf1o  6021  undifixp  7090  dfdom2  7125  sbthlem5  7213  sbthlem6  7214  domunsn  7249  fodomr  7250  mapdom2  7270  limensuci  7275  findcard2  7340  unfi  7366  marypha1lem  7430  brwdom2  7533  infdifsn  7603  cantnfrescl  7624  ackbij1lem12  8103  ackbij1lem18  8109  ssfin4  8182  fin23lem28  8212  fin23lem30  8214  fin1a2lem13  8284  canthp1lem1  8519  xrsupss  10879  xrinfmss  10880  hashssdif  11669  hashfun  11692  hashf1lem2  11697  fsumless  12567  incexclem  12608  incexc  12609  isclo  17143  cmpcld  17457  uniiccmbl  19474  itgss3  19698  dchreq  21034  indval2  24404  esummono  24442  gsumesum  24443  sigaclfu2  24496  measxun2  24556  measvuni  24560  measssd  24561  axlowdimlem7  25879  axlowdimlem10  25882  ralxpmap  26733  diophrw  26808  eldioph2lem1  26809  eldioph2lem2  26810  kelac1  27129  pwssplit1  27156  frlmsslss2  27213
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1555  ax-5 1566  ax-17 1626  ax-9 1666  ax-8 1687  ax-6 1744  ax-7 1749  ax-11 1761  ax-12 1950  ax-ext 2416
This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-tru 1328  df-ex 1551  df-nf 1554  df-sb 1659  df-clab 2422  df-cleq 2428  df-clel 2431  df-nfc 2560  df-ne 2600  df-ral 2702  df-rab 2706  df-v 2950  df-dif 3315  df-un 3317  df-in 3319  df-ss 3326  df-nul 3621
  Copyright terms: Public domain W3C validator