Theorem undif 4434

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 4138	. 2 ⊢ (𝐴 ⊆ 𝐵 ↔ (𝐴 ∪ 𝐵) = 𝐵)
2		undif2 4429	. . 3 ⊢ (𝐴 ∪ (𝐵 ∖ 𝐴)) = (𝐴 ∪ 𝐵)
3	2	eqeq1i 2741	. 2 ⊢ ((𝐴 ∪ (𝐵 ∖ 𝐴)) = 𝐵 ↔ (𝐴 ∪ 𝐵) = 𝐵)
4	1, 3	bitr4i 278	1 ⊢ (𝐴 ⊆ 𝐵 ↔ (𝐴 ∪ (𝐵 ∖ 𝐴)) = 𝐵)

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

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 2115  ax-9 2123  ax-ext 2708

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 2715  df-cleq 2728  df-clel 2811  df-rab 3400  df-v 3442  df-dif 3904  df-un 3906  df-in 3908  df-ss 3918  df-nul 4286

This theorem is referenced by:  undifrOLD  4436  raldifeq  4446  pwundif  4578  imadifssran  6109  fveqf1o  7248  undifixp  8872  dfdom2  8915  sbthlem5  9019  sbthlem6  9020  domunsn  9055  fodomr  9056  mapdom2  9076  limensuci  9081  findcard2  9089  ssfi  9097  fodomfir  9228  marypha1lem  9336  brwdom2  9478  infdifsn  9566  ackbij1lem12  10140  ackbij1lem18  10146  ssfin4  10220  fin23lem28  10250  fin23lem30  10252  fin1a2lem13  10322  canthp1lem1  10563  xrsupss  13224  xrinfmss  13225  hashssdif  14335  hashfun  14360  hashf1lem2  14379  fsumsplit1  15668  fsumless  15719  incexclem  15759  incexc  15760  fprodsplit1f  15913  pwssplit1  21011  frlmsslss2  21730  mdetdiaglem  22542  mdetrlin  22546  mdetrsca  22547  mdetralt  22552  smadiadet  22614  isclo  23031  cmpcld  23346  rrxcph  25348  rrxdstprj1  25365  uniiccmbl  25547  itgss3  25772  dchreq  27225  noextendseq  27635  madeun  27880  axlowdimlem7  29021  axlowdimlem10  29024  fressupp  32767  padct  32797  resf1o  32809  fprodeq02  32904  indval2  32933  gsummptres2  33136  cycpmcl  33198  cycpmco2  33215  cyc3co2  33222  cycpmconjslem2  33237  cyc3conja  33239  elrspunidl  33509  lbsdiflsp0  33783  dimkerim  33784  locfinref  33998  esummono  34211  gsumesum  34216  sigaclfu2  34278  measxun2  34367  measvuni  34371  measssd  34372  pmeasmono  34481  eulerpartlemt  34528  tgoldbachgtde  34817  satfvsucsuc  35559  poimirlem9  37826  poimirlem15  37832  poimirlem25  37842  selvvvval  42824  evlselv  42826  fsuppssind  42832  diophrw  42997  eldioph2lem1  42998  eldioph2lem2  42999  kelac1  43301  tfsconcatfn  43576  tfsconcatrev  43586  ioccncflimc  46125  icocncflimc  46129  dirkercncflem2  46344  dirkercncflem3  46345  sge0ss  46652  meassle  46703  meadif  46719  meaiininclem  46726  isomenndlem  46770  hspmbllem1  46866  hspmbllem2  46867  ovolval4lem1  46889  fsumsplitsndif  47615  stgrclnbgr0  48207