Theorem undif 4436

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

Syntax hints:   ↔ wb 206   = wceq 1542   ∖ cdif 3900   ∪ cun 3901   ⊆ wss 3903

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-tru 1545  df-fal 1555  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-rab 3402  df-v 3444  df-dif 3906  df-un 3908  df-in 3910  df-ss 3920  df-nul 4288

This theorem is referenced by:  undifrOLD  4438  raldifeq  4448  pwundif  4580  imadifssran  6117  fveqf1o  7258  undifixp  8884  dfdom2  8927  sbthlem5  9031  sbthlem6  9032  domunsn  9067  fodomr  9068  mapdom2  9088  limensuci  9093  findcard2  9101  ssfi  9109  fodomfir  9240  marypha1lem  9348  brwdom2  9490  infdifsn  9578  ackbij1lem12  10152  ackbij1lem18  10158  ssfin4  10232  fin23lem28  10262  fin23lem30  10264  fin1a2lem13  10334  canthp1lem1  10575  xrsupss  13236  xrinfmss  13237  hashssdif  14347  hashfun  14372  hashf1lem2  14391  fsumsplit1  15680  fsumless  15731  incexclem  15771  incexc  15772  fprodsplit1f  15925  pwssplit1  21023  frlmsslss2  21742  mdetdiaglem  22554  mdetrlin  22558  mdetrsca  22559  mdetralt  22564  smadiadet  22626  isclo  23043  cmpcld  23358  rrxcph  25360  rrxdstprj1  25377  uniiccmbl  25559  itgss3  25784  dchreq  27237  noextendseq  27647  madeun  27892  axlowdimlem7  29033  axlowdimlem10  29036  fressupp  32777  padct  32807  resf1o  32819  fprodeq02  32914  indval2  32943  gsummptres2  33146  cycpmcl  33209  cycpmco2  33226  cyc3co2  33233  cycpmconjslem2  33248  cyc3conja  33250  elrspunidl  33520  lbsdiflsp0  33803  dimkerim  33804  locfinref  34018  esummono  34231  gsumesum  34236  sigaclfu2  34298  measxun2  34387  measvuni  34391  measssd  34392  pmeasmono  34501  eulerpartlemt  34548  tgoldbachgtde  34837  satfvsucsuc  35578  poimirlem9  37874  poimirlem15  37880  poimirlem25  37890  selvvvval  42937  evlselv  42939  fsuppssind  42945  diophrw  43110  eldioph2lem1  43111  eldioph2lem2  43112  kelac1  43414  tfsconcatfn  43689  tfsconcatrev  43699  ioccncflimc  46237  icocncflimc  46241  dirkercncflem2  46456  dirkercncflem3  46457  sge0ss  46764  meassle  46815  meadif  46831  meaiininclem  46838  isomenndlem  46882  hspmbllem1  46978  hspmbllem2  46979  ovolval4lem1  47001  fsumsplitsndif  47727  stgrclnbgr0  48319