Theorem undif 4482

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

Syntax hints:   ↔ wb 206   = wceq 1540   ∖ cdif 3948   ∪ cun 3949   ⊆ wss 3951

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2065  df-clab 2715  df-cleq 2729  df-clel 2816  df-rab 3437  df-v 3482  df-dif 3954  df-un 3956  df-in 3958  df-ss 3968  df-nul 4334

This theorem is referenced by:  undifrOLD  4484  raldifeq  4494  pwundif  4624  imadifssran  6171  fveqf1o  7322  undifixp  8974  dfdom2  9018  sbthlem5  9127  sbthlem6  9128  domunsn  9167  fodomr  9168  mapdom2  9188  limensuci  9193  findcard2  9204  ssfi  9213  fodomfir  9368  marypha1lem  9473  brwdom2  9613  infdifsn  9697  ackbij1lem12  10270  ackbij1lem18  10276  ssfin4  10350  fin23lem28  10380  fin23lem30  10382  fin1a2lem13  10452  canthp1lem1  10692  xrsupss  13351  xrinfmss  13352  hashssdif  14451  hashfun  14476  hashf1lem2  14495  fsumsplit1  15781  fsumless  15832  incexclem  15872  incexc  15873  fprodsplit1f  16026  pwssplit1  21058  frlmsslss2  21795  mdetdiaglem  22604  mdetrlin  22608  mdetrsca  22609  mdetralt  22614  smadiadet  22676  isclo  23095  cmpcld  23410  rrxcph  25426  rrxdstprj1  25443  uniiccmbl  25625  itgss3  25850  dchreq  27302  noextendseq  27712  madeun  27922  axlowdimlem7  28963  axlowdimlem10  28966  fressupp  32697  padct  32731  resf1o  32741  fprodeq02  32825  indval2  32839  gsummptres2  33056  cycpmcl  33136  cycpmco2  33153  cyc3co2  33160  cycpmconjslem2  33175  cyc3conja  33177  elrspunidl  33456  lbsdiflsp0  33677  dimkerim  33678  locfinref  33840  esummono  34055  gsumesum  34060  sigaclfu2  34122  measxun2  34211  measvuni  34215  measssd  34216  pmeasmono  34326  eulerpartlemt  34373  tgoldbachgtde  34675  satfvsucsuc  35370  poimirlem9  37636  poimirlem15  37642  poimirlem25  37652  selvvvval  42595  evlselv  42597  fsuppssind  42603  diophrw  42770  eldioph2lem1  42771  eldioph2lem2  42772  kelac1  43075  tfsconcatfn  43351  tfsconcatrev  43361  ioccncflimc  45900  icocncflimc  45904  dirkercncflem2  46119  dirkercncflem3  46120  sge0ss  46427  meassle  46478  meadif  46494  meaiininclem  46501  isomenndlem  46545  hspmbllem1  46641  hspmbllem2  46642  ovolval4lem1  46664  fsumsplitsndif  47360  stgrclnbgr0  47932