Theorem undif 4421

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

Syntax hints:   ↔ wb 205   = wceq 1542   ∖ cdif 3889   ∪ cun 3890   ⊆ wss 3892

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1975  ax-7 2015  ax-8 2112  ax-9 2120  ax-ext 2711

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-tru 1545  df-fal 1555  df-ex 1787  df-sb 2072  df-clab 2718  df-cleq 2732  df-clel 2818  df-rab 3075  df-v 3433  df-dif 3895  df-un 3897  df-in 3899  df-ss 3909  df-nul 4263

This theorem is referenced by:  raldifeq  4430  pwundif  4565  difsnid  4749  fveqf1o  7172  f1ofvswap  7175  ralxpmap  8676  undifixp  8714  dfdom2  8758  sbthlem5  8865  sbthlem6  8866  domunsn  8905  fodomr  8906  mapdom2  8926  limensuci  8931  findcard2  8938  ssfi  8947  findcard2OLD  9044  unfiOLD  9069  marypha1lem  9180  brwdom2  9320  infdifsn  9403  ackbij1lem12  9998  ackbij1lem18  10004  ssfin4  10077  fin23lem28  10107  fin23lem30  10109  fin1a2lem13  10179  canthp1lem1  10419  xrsupss  13054  xrinfmss  13055  hashssdif  14138  hashfun  14163  hashf1lem2  14181  fsumsplit1  15468  fsumless  15519  incexclem  15559  incexc  15560  fprodsplit1f  15711  pwssplit1  20332  frlmsslss2  20993  mdetdiaglem  21758  mdetrlin  21762  mdetrsca  21763  mdetralt  21768  smadiadet  21830  isclo  22249  cmpcld  22564  rrxcph  24567  rrxdstprj1  24584  uniiccmbl  24765  itgss3  24990  dchreq  26417  axlowdimlem7  27327  axlowdimlem10  27330  undifr  30881  fressupp  31031  padct  31063  resf1o  31074  fprodeq02  31146  gsummptres2  31322  cycpmcl  31392  cycpmco2  31409  cyc3co2  31416  cycpmconjslem2  31431  cyc3conja  31433  elrspunidl  31615  lbsdiflsp0  31716  dimkerim  31717  locfinref  31800  indval2  31991  esummono  32031  gsumesum  32036  sigaclfu2  32098  measxun2  32187  measvuni  32191  measssd  32192  pmeasmono  32300  eulerpartlemt  32347  tgoldbachgtde  32649  satfvsucsuc  33336  noextendseq  33879  madeun  34075  poimirlem9  35795  poimirlem15  35801  poimirlem25  35811  fsuppssind  40291  diophrw  40590  eldioph2lem1  40591  eldioph2lem2  40592  kelac1  40897  ioccncflimc  43408  icocncflimc  43412  dirkercncflem2  43627  dirkercncflem3  43628  sge0ss  43932  meassle  43983  meadif  43999  meaiininclem  44006  isomenndlem  44050  hspmbllem1  44146  hspmbllem2  44147  ovolval4lem1  44169  fsumsplitsndif  44804