Theorem undif 4396

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

Syntax hints:   ↔ wb 209   = wceq 1543   ∖ cdif 3863   ∪ cun 3864   ⊆ wss 3866

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918  ax-6 1976  ax-7 2016  ax-8 2112  ax-9 2120  ax-ext 2708

This theorem depends on definitions:  df-bi 210  df-an 400  df-or 848  df-tru 1546  df-fal 1556  df-ex 1788  df-sb 2071  df-clab 2715  df-cleq 2729  df-clel 2816  df-rab 3070  df-v 3410  df-dif 3869  df-un 3871  df-in 3873  df-ss 3883  df-nul 4238

This theorem is referenced by:  raldifeq  4405  pwundif  4539  difsnid  4723  fveqf1o  7113  f1ofvswap  7116  ralxpmap  8577  undifixp  8615  dfdom2  8654  sbthlem5  8760  sbthlem6  8761  domunsn  8796  fodomr  8797  mapdom2  8817  limensuci  8822  findcard2  8842  ssfi  8851  findcard2OLD  8913  unfiOLD  8938  marypha1lem  9049  brwdom2  9189  infdifsn  9272  ackbij1lem12  9845  ackbij1lem18  9851  ssfin4  9924  fin23lem28  9954  fin23lem30  9956  fin1a2lem13  10026  canthp1lem1  10266  xrsupss  12899  xrinfmss  12900  hashssdif  13979  hashfun  14004  hashf1lem2  14022  fsumsplit1  15309  fsumless  15360  incexclem  15400  incexc  15401  fprodsplit1f  15552  pwssplit1  20096  frlmsslss2  20737  mdetdiaglem  21495  mdetrlin  21499  mdetrsca  21500  mdetralt  21505  smadiadet  21567  isclo  21984  cmpcld  22299  rrxcph  24289  rrxdstprj1  24306  uniiccmbl  24487  itgss3  24712  dchreq  26139  axlowdimlem7  27039  axlowdimlem10  27042  undifr  30591  fressupp  30742  padct  30774  resf1o  30785  fprodeq02  30857  gsummptres2  31032  cycpmcl  31102  cycpmco2  31119  cyc3co2  31126  cycpmconjslem2  31141  cyc3conja  31143  elrspunidl  31320  lbsdiflsp0  31421  dimkerim  31422  locfinref  31505  indval2  31694  esummono  31734  gsumesum  31739  sigaclfu2  31801  measxun2  31890  measvuni  31894  measssd  31895  pmeasmono  32003  eulerpartlemt  32050  tgoldbachgtde  32352  satfvsucsuc  33040  noextendseq  33607  madeun  33803  poimirlem9  35523  poimirlem15  35529  poimirlem25  35539  fsuppssind  39992  diophrw  40284  eldioph2lem1  40285  eldioph2lem2  40286  kelac1  40591  ioccncflimc  43101  icocncflimc  43105  dirkercncflem2  43320  dirkercncflem3  43321  sge0ss  43625  meassle  43676  meadif  43692  meaiininclem  43699  isomenndlem  43743  hspmbllem1  43839  hspmbllem2  43840  ovolval4lem1  43862  fsumsplitsndif  44498