Theorem undif 4481

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 4180	. 2 ⊢ (𝐴 ⊆ 𝐵 ↔ (𝐴 ∪ 𝐵) = 𝐵)
2		undif2 4476	. . 3 ⊢ (𝐴 ∪ (𝐵 ∖ 𝐴)) = (𝐴 ∪ 𝐵)
3	2	eqeq1i 2737	. 2 ⊢ ((𝐴 ∪ (𝐵 ∖ 𝐴)) = 𝐵 ↔ (𝐴 ∪ 𝐵) = 𝐵)
4	1, 3	bitr4i 277	1 ⊢ (𝐴 ⊆ 𝐵 ↔ (𝐴 ∪ (𝐵 ∖ 𝐴)) = 𝐵)

Syntax hints:   ↔ wb 205   = wceq 1541   ∖ cdif 3945   ∪ cun 3946   ⊆ wss 3948

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 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2703

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-tru 1544  df-fal 1554  df-ex 1782  df-sb 2068  df-clab 2710  df-cleq 2724  df-clel 2810  df-rab 3433  df-v 3476  df-dif 3951  df-un 3953  df-in 3955  df-ss 3965  df-nul 4323

This theorem is referenced by:  undifrOLD  4483  raldifeq  4493  pwundif  4626  fveqf1o  7303  undifixp  8930  dfdom2  8976  sbthlem5  9089  sbthlem6  9090  domunsn  9129  fodomr  9130  mapdom2  9150  limensuci  9155  findcard2  9166  ssfi  9175  findcard2OLD  9286  unfiOLD  9315  marypha1lem  9430  brwdom2  9570  infdifsn  9654  ackbij1lem12  10228  ackbij1lem18  10234  ssfin4  10307  fin23lem28  10337  fin23lem30  10339  fin1a2lem13  10409  canthp1lem1  10649  xrsupss  13292  xrinfmss  13293  hashssdif  14376  hashfun  14401  hashf1lem2  14421  fsumsplit1  15695  fsumless  15746  incexclem  15786  incexc  15787  fprodsplit1f  15938  pwssplit1  20814  frlmsslss2  21549  mdetdiaglem  22320  mdetrlin  22324  mdetrsca  22325  mdetralt  22330  smadiadet  22392  isclo  22811  cmpcld  23126  rrxcph  25133  rrxdstprj1  25150  uniiccmbl  25331  itgss3  25556  dchreq  26985  noextendseq  27394  madeun  27603  axlowdimlem7  28461  axlowdimlem10  28464  fressupp  32165  padct  32199  resf1o  32210  fprodeq02  32284  gsummptres2  32463  cycpmcl  32533  cycpmco2  32550  cyc3co2  32557  cycpmconjslem2  32572  cyc3conja  32574  elrspunidl  32808  lbsdiflsp0  32987  dimkerim  32988  locfinref  33107  indval2  33298  esummono  33338  gsumesum  33343  sigaclfu2  33405  measxun2  33494  measvuni  33498  measssd  33499  pmeasmono  33609  eulerpartlemt  33656  tgoldbachgtde  33958  satfvsucsuc  34642  poimirlem9  36800  poimirlem15  36806  poimirlem25  36816  selvvvval  41459  evlselv  41461  fsuppssind  41467  diophrw  41799  eldioph2lem1  41800  eldioph2lem2  41801  kelac1  42107  tfsconcatfn  42390  tfsconcatrev  42400  ioccncflimc  44900  icocncflimc  44904  dirkercncflem2  45119  dirkercncflem3  45120  sge0ss  45427  meassle  45478  meadif  45494  meaiininclem  45501  isomenndlem  45545  hspmbllem1  45641  hspmbllem2  45642  ovolval4lem1  45664  fsumsplitsndif  46340