Theorem undif 4487

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

Syntax hints:   ↔ wb 206   = wceq 1536   ∖ cdif 3959   ∪ cun 3960   ⊆ wss 3962

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1791  ax-4 1805  ax-5 1907  ax-6 1964  ax-7 2004  ax-8 2107  ax-9 2115  ax-ext 2705

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-tru 1539  df-fal 1549  df-ex 1776  df-sb 2062  df-clab 2712  df-cleq 2726  df-clel 2813  df-rab 3433  df-v 3479  df-dif 3965  df-un 3967  df-in 3969  df-ss 3979  df-nul 4339

This theorem is referenced by:  undifrOLD  4489  raldifeq  4499  pwundif  4628  fveqf1o  7321  undifixp  8972  dfdom2  9016  sbthlem5  9125  sbthlem6  9126  domunsn  9165  fodomr  9166  mapdom2  9186  limensuci  9191  findcard2  9202  ssfi  9211  fodomfir  9365  marypha1lem  9470  brwdom2  9610  infdifsn  9694  ackbij1lem12  10267  ackbij1lem18  10273  ssfin4  10347  fin23lem28  10377  fin23lem30  10379  fin1a2lem13  10449  canthp1lem1  10689  xrsupss  13347  xrinfmss  13348  hashssdif  14447  hashfun  14472  hashf1lem2  14491  fsumsplit1  15777  fsumless  15828  incexclem  15868  incexc  15869  fprodsplit1f  16022  pwssplit1  21075  frlmsslss2  21812  mdetdiaglem  22619  mdetrlin  22623  mdetrsca  22624  mdetralt  22629  smadiadet  22691  isclo  23110  cmpcld  23425  rrxcph  25439  rrxdstprj1  25456  uniiccmbl  25638  itgss3  25864  dchreq  27316  noextendseq  27726  madeun  27936  axlowdimlem7  28977  axlowdimlem10  28980  fressupp  32702  padct  32736  resf1o  32747  fprodeq02  32829  gsummptres2  33038  cycpmcl  33118  cycpmco2  33135  cyc3co2  33142  cycpmconjslem2  33157  cyc3conja  33159  elrspunidl  33435  lbsdiflsp0  33653  dimkerim  33654  locfinref  33801  indval2  33994  esummono  34034  gsumesum  34039  sigaclfu2  34101  measxun2  34190  measvuni  34194  measssd  34195  pmeasmono  34305  eulerpartlemt  34352  tgoldbachgtde  34653  satfvsucsuc  35349  poimirlem9  37615  poimirlem15  37621  poimirlem25  37631  selvvvval  42571  evlselv  42573  fsuppssind  42579  diophrw  42746  eldioph2lem1  42747  eldioph2lem2  42748  kelac1  43051  tfsconcatfn  43327  tfsconcatrev  43337  ioccncflimc  45840  icocncflimc  45844  dirkercncflem2  46059  dirkercncflem3  46060  sge0ss  46367  meassle  46418  meadif  46434  meaiininclem  46441  isomenndlem  46485  hspmbllem1  46581  hspmbllem2  46582  ovolval4lem1  46604  fsumsplitsndif  47297  stgrclnbgr0  47867