Theorem undif 4448

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

Syntax hints:   ↔ wb 206   = wceq 1540   ∖ cdif 3914   ∪ cun 3915   ⊆ wss 3917

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 2008  ax-8 2111  ax-9 2119  ax-ext 2702

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2066  df-clab 2709  df-cleq 2722  df-clel 2804  df-rab 3409  df-v 3452  df-dif 3920  df-un 3922  df-in 3924  df-ss 3934  df-nul 4300

This theorem is referenced by:  undifrOLD  4450  raldifeq  4460  pwundif  4590  imadifssran  6127  fveqf1o  7280  undifixp  8910  dfdom2  8952  sbthlem5  9061  sbthlem6  9062  domunsn  9097  fodomr  9098  mapdom2  9118  limensuci  9123  findcard2  9134  ssfi  9143  fodomfir  9286  marypha1lem  9391  brwdom2  9533  infdifsn  9617  ackbij1lem12  10190  ackbij1lem18  10196  ssfin4  10270  fin23lem28  10300  fin23lem30  10302  fin1a2lem13  10372  canthp1lem1  10612  xrsupss  13276  xrinfmss  13277  hashssdif  14384  hashfun  14409  hashf1lem2  14428  fsumsplit1  15718  fsumless  15769  incexclem  15809  incexc  15810  fprodsplit1f  15963  pwssplit1  20973  frlmsslss2  21691  mdetdiaglem  22492  mdetrlin  22496  mdetrsca  22497  mdetralt  22502  smadiadet  22564  isclo  22981  cmpcld  23296  rrxcph  25299  rrxdstprj1  25316  uniiccmbl  25498  itgss3  25723  dchreq  27176  noextendseq  27586  madeun  27802  axlowdimlem7  28882  axlowdimlem10  28885  fressupp  32618  padct  32650  resf1o  32660  fprodeq02  32755  indval2  32784  gsummptres2  33000  cycpmcl  33080  cycpmco2  33097  cyc3co2  33104  cycpmconjslem2  33119  cyc3conja  33121  elrspunidl  33406  lbsdiflsp0  33629  dimkerim  33630  locfinref  33838  esummono  34051  gsumesum  34056  sigaclfu2  34118  measxun2  34207  measvuni  34211  measssd  34212  pmeasmono  34322  eulerpartlemt  34369  tgoldbachgtde  34658  satfvsucsuc  35359  poimirlem9  37630  poimirlem15  37636  poimirlem25  37646  selvvvval  42580  evlselv  42582  fsuppssind  42588  diophrw  42754  eldioph2lem1  42755  eldioph2lem2  42756  kelac1  43059  tfsconcatfn  43334  tfsconcatrev  43344  ioccncflimc  45890  icocncflimc  45894  dirkercncflem2  46109  dirkercncflem3  46110  sge0ss  46417  meassle  46468  meadif  46484  meaiininclem  46491  isomenndlem  46535  hspmbllem1  46631  hspmbllem2  46632  ovolval4lem1  46654  fsumsplitsndif  47378  stgrclnbgr0  47968