Theorem undif 4420

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

Syntax hints:   ↔ wb 205   = wceq 1541   ∖ cdif 3888   ∪ cun 3889   ⊆ wss 3891

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1801  ax-4 1815  ax-5 1916  ax-6 1974  ax-7 2014  ax-8 2111  ax-9 2119  ax-ext 2710

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 844  df-tru 1544  df-fal 1554  df-ex 1786  df-sb 2071  df-clab 2717  df-cleq 2731  df-clel 2817  df-rab 3074  df-v 3432  df-dif 3894  df-un 3896  df-in 3898  df-ss 3908  df-nul 4262

This theorem is referenced by:  raldifeq  4429  pwundif  4564  difsnid  4748  fveqf1o  7168  f1ofvswap  7171  ralxpmap  8658  undifixp  8696  dfdom2  8737  sbthlem5  8843  sbthlem6  8844  domunsn  8879  fodomr  8880  mapdom2  8900  limensuci  8905  findcard2  8912  ssfi  8921  findcard2OLD  9017  unfiOLD  9042  marypha1lem  9153  brwdom2  9293  infdifsn  9376  ackbij1lem12  9971  ackbij1lem18  9977  ssfin4  10050  fin23lem28  10080  fin23lem30  10082  fin1a2lem13  10152  canthp1lem1  10392  xrsupss  13025  xrinfmss  13026  hashssdif  14108  hashfun  14133  hashf1lem2  14151  fsumsplit1  15438  fsumless  15489  incexclem  15529  incexc  15530  fprodsplit1f  15681  pwssplit1  20302  frlmsslss2  20963  mdetdiaglem  21728  mdetrlin  21732  mdetrsca  21733  mdetralt  21738  smadiadet  21800  isclo  22219  cmpcld  22534  rrxcph  24537  rrxdstprj1  24554  uniiccmbl  24735  itgss3  24960  dchreq  26387  axlowdimlem7  27297  axlowdimlem10  27300  undifr  30851  fressupp  31001  padct  31033  resf1o  31044  fprodeq02  31116  gsummptres2  31292  cycpmcl  31362  cycpmco2  31379  cyc3co2  31386  cycpmconjslem2  31401  cyc3conja  31403  elrspunidl  31585  lbsdiflsp0  31686  dimkerim  31687  locfinref  31770  indval2  31961  esummono  32001  gsumesum  32006  sigaclfu2  32068  measxun2  32157  measvuni  32161  measssd  32162  pmeasmono  32270  eulerpartlemt  32317  tgoldbachgtde  32619  satfvsucsuc  33306  noextendseq  33849  madeun  34045  poimirlem9  35765  poimirlem15  35771  poimirlem25  35781  fsuppssind  40262  diophrw  40561  eldioph2lem1  40562  eldioph2lem2  40563  kelac1  40868  ioccncflimc  43380  icocncflimc  43384  dirkercncflem2  43599  dirkercncflem3  43600  sge0ss  43904  meassle  43955  meadif  43971  meaiininclem  43978  isomenndlem  44022  hspmbllem1  44118  hspmbllem2  44119  ovolval4lem1  44141  fsumsplitsndif  44777