Theorem undif 4438

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 4132	. 2 ⊢ (𝐴 ⊆ 𝐵 ↔ (𝐴 ∪ 𝐵) = 𝐵)
2		undif2 4431	. . 3 ⊢ (𝐴 ∪ (𝐵 ∖ 𝐴)) = (𝐴 ∪ 𝐵)
3	2	eqeq1i 2766	. 2 ⊢ ((𝐴 ∪ (𝐵 ∖ 𝐴)) = 𝐵 ↔ (𝐴 ∪ 𝐵) = 𝐵)
4	1, 3	bitr4i 281	1 ⊢ (𝐴 ⊆ 𝐵 ↔ (𝐴 ∪ (𝐵 ∖ 𝐴)) = 𝐵)

This proof depends on syntax axioms:   ↔ wb 209   = wceq 1570   ∖ cdif 3896   ∪ cun 3897   ⊆ wss 3899

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2733

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-tru 1573  df-fal 1583  df-ex 1813  df-sb 2100  df-clab 2740  df-cleq 2753  df-clel 2836  df-rab 3414  df-v 3453  df-dif 3902  df-un 3904  df-in 3906  df-ss 3916  df-nul 4280

This theorem is used by:  raldifeq  4449  pwundif  4582  imadifssranOLD  6196  fveqf1o  7302  undifixp  8946  dfdom2  8989  sbthlem5  9094  sbthlem6  9095  domunsn  9130  fodomr  9131  mapdom2  9151  limensuci  9156  findcard2  9164  ssfi  9172  fodomfir  9303  marypha1lem  9409  brwdom2  9551  infdifsn  9642  ackbij1lem12  10289  ackbij1lem18  10295  ssfin4  10369  fin23lem28  10399  fin23lem30  10401  fin1a2lem13  10471  canthp1lem1  10718  indval2  12306  xrsupss  13420  xrinfmss  13421  hashssdif  14537  hashfun  14562  hashf1lem2  14581  fsumsplit1  15891  fsumless  15943  incexclem  15985  incexc  15986  fprodsplit1f  16137  pwssplit1  21314  frlmsslss2  22061  selvvvval  22431  mdetdiaglem  22893  mdetrlin  22897  mdetrsca  22898  mdetralt  22903  smadiadet  22965  isclo  23385  cmpcld  23700  rrxcph  25693  rrxdstprj1  25710  uniiccmbl  25891  itgss3  26115  dchreq  27567  noextendseq  28006  madeun  28252  axlowdimlem7  29508  axlowdimlem10  29511  fressupp  33263  padct  33292  resf1o  33304  fprodeq02  33397  gsummptres2  33596  cycpmcl  33659  cycpmco2  33676  cyc3co2  33683  cycpmconjslem2  33698  cyc3conja  33700  elrspunidl  33960  lbsdiflsp0  34240  dimkerim  34241  locfinref  34455  esummono  34668  gsumesum  34673  sigaclfu2  34735  measxun2  34825  measvuni  34829  measssd  34830  pmeasmono  34939  eulerpartlemt  34986  tgoldbachgtde  35272  satfvsucsuc  36099  poimirlem9  38515  poimirlem15  38521  poimirlem25  38531  evlselv  43579  fsuppssind  43583  diophrw  43723  eldioph2lem1  43724  eldioph2lem2  43725  kelac1  44023  tfsconcatfn  44298  tfsconcatrev  44308  ioccncflimc  46839  icocncflimc  46843  dirkercncflem2  47058  dirkercncflem3  47059  sge0ss  47366  meassle  47417  meadif  47433  meaiininclem  47440  isomenndlem  47484  hspmbllem1  47580  hspmbllem2  47581  ovolval4lem1  47603  fsumsplitsndif  48395  stgrclnbgr0  49007