Theorem undif 4432

Description: Union of complementary parts into whole. (Contributed by NM, 22-Mar-1998.)

Assertion

Ref	Expression
undif	⊢ (𝐴 ⊆ 𝐵 ↔ (𝐴 ∪ (𝐵 ∖ 𝐴)) = 𝐵)

Proof of Theorem undif

Step	Hyp	Ref	Expression
1		ssequn1 4136	. 2 ⊢ (𝐴 ⊆ 𝐵 ↔ (𝐴 ∪ 𝐵) = 𝐵)
2		undif2 4427	. . 3 ⊢ (𝐴 ∪ (𝐵 ∖ 𝐴)) = (𝐴 ∪ 𝐵)
3	2	eqeq1i 2736	. 2 ⊢ ((𝐴 ∪ (𝐵 ∖ 𝐴)) = 𝐵 ↔ (𝐴 ∪ 𝐵) = 𝐵)
4	1, 3	bitr4i 278	1 ⊢ (𝐴 ⊆ 𝐵 ↔ (𝐴 ∪ (𝐵 ∖ 𝐴)) = 𝐵)

Syntax hints:   ↔ wb 206   = wceq 1541   ∖ cdif 3899   ∪ cun 3900   ⊆ wss 3902

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2113  ax-9 2121  ax-ext 2703

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-tru 1544  df-fal 1554  df-ex 1781  df-sb 2068  df-clab 2710  df-cleq 2723  df-clel 2806  df-rab 3396  df-v 3438  df-dif 3905  df-un 3907  df-in 3909  df-ss 3919  df-nul 4284

This theorem is referenced by:  undifrOLD  4434  raldifeq  4444  pwundif  4574  imadifssran  6098  fveqf1o  7236  undifixp  8858  dfdom2  8900  sbthlem5  9004  sbthlem6  9005  domunsn  9040  fodomr  9041  mapdom2  9061  limensuci  9066  findcard2  9074  ssfi  9082  fodomfir  9212  marypha1lem  9317  brwdom2  9459  infdifsn  9547  ackbij1lem12  10121  ackbij1lem18  10127  ssfin4  10201  fin23lem28  10231  fin23lem30  10233  fin1a2lem13  10303  canthp1lem1  10543  xrsupss  13208  xrinfmss  13209  hashssdif  14319  hashfun  14344  hashf1lem2  14363  fsumsplit1  15652  fsumless  15703  incexclem  15743  incexc  15744  fprodsplit1f  15897  pwssplit1  20994  frlmsslss2  21713  mdetdiaglem  22514  mdetrlin  22518  mdetrsca  22519  mdetralt  22524  smadiadet  22586  isclo  23003  cmpcld  23318  rrxcph  25320  rrxdstprj1  25337  uniiccmbl  25519  itgss3  25744  dchreq  27197  noextendseq  27607  madeun  27830  axlowdimlem7  28927  axlowdimlem10  28930  fressupp  32667  padct  32699  resf1o  32711  fprodeq02  32804  indval2  32833  gsummptres2  33031  cycpmcl  33083  cycpmco2  33100  cyc3co2  33107  cycpmconjslem2  33122  cyc3conja  33124  elrspunidl  33391  lbsdiflsp0  33637  dimkerim  33638  locfinref  33852  esummono  34065  gsumesum  34070  sigaclfu2  34132  measxun2  34221  measvuni  34225  measssd  34226  pmeasmono  34335  eulerpartlemt  34382  tgoldbachgtde  34671  satfvsucsuc  35407  poimirlem9  37675  poimirlem15  37681  poimirlem25  37691  selvvvval  42624  evlselv  42626  fsuppssind  42632  diophrw  42798  eldioph2lem1  42799  eldioph2lem2  42800  kelac1  43102  tfsconcatfn  43377  tfsconcatrev  43387  ioccncflimc  45929  icocncflimc  45933  dirkercncflem2  46148  dirkercncflem3  46149  sge0ss  46456  meassle  46507  meadif  46523  meaiininclem  46530  isomenndlem  46574  hspmbllem1  46670  hspmbllem2  46671  ovolval4lem1  46693  fsumsplitsndif  47410  stgrclnbgr0  48002