Theorem undif 4426

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 4129	. 2 ⊢ (𝐴 ⊆ 𝐵 ↔ (𝐴 ∪ 𝐵) = 𝐵)
2		undif2 4421	. . 3 ⊢ (𝐴 ∪ (𝐵 ∖ 𝐴)) = (𝐴 ∪ 𝐵)
3	2	eqeq1i 2757	. 2 ⊢ ((𝐴 ∪ (𝐵 ∖ 𝐴)) = 𝐵 ↔ (𝐴 ∪ 𝐵) = 𝐵)
4	1, 3	bitr4i 280	1 ⊢ (𝐴 ⊆ 𝐵 ↔ (𝐴 ∪ (𝐵 ∖ 𝐴)) = 𝐵)

Syntax hints:   ↔ wb 208   = wceq 1550   ∖ cdif 3892   ∪ cun 3893   ⊆ wss 3895

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1805  ax-4 1819  ax-5 1920  ax-6 1977  ax-7 2018  ax-8 2134  ax-9 2142  ax-ext 2724

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 857  df-tru 1553  df-fal 1563  df-ex 1790  df-sb 2081  df-clab 2731  df-cleq 2744  df-clel 2827  df-rab 3405  df-v 3446  df-dif 3898  df-un 3900  df-in 3902  df-ss 3912  df-nul 4277

This theorem is referenced by:  raldifeq  4437  pwundif  4570  imadifssran  6122  fveqf1o  7271  undifixp  8901  dfdom2  8944  sbthlem5  9048  sbthlem6  9049  domunsn  9084  fodomr  9085  mapdom2  9105  limensuci  9110  findcard2  9118  ssfi  9126  fodomfir  9257  marypha1lem  9365  brwdom2  9507  infdifsn  9598  ackbij1lem12  10172  ackbij1lem18  10178  ssfin4  10253  fin23lem28  10283  fin23lem30  10285  fin1a2lem13  10355  canthp1lem1  10596  indval2  12186  xrsupss  13298  xrinfmss  13299  hashssdif  14411  hashfun  14436  hashf1lem2  14455  fsumsplit1  15744  fsumless  15796  incexclem  15838  incexc  15839  fprodsplit1f  15992  pwssplit1  21095  frlmsslss2  21796  selvvvval  22164  mdetdiaglem  22627  mdetrlin  22631  mdetrsca  22632  mdetralt  22637  smadiadet  22699  isclo  23116  cmpcld  23431  rrxcph  25423  rrxdstprj1  25440  uniiccmbl  25621  itgss3  25846  dchreq  27288  noextendseq  27697  madeun  27943  axlowdimlem7  29084  axlowdimlem10  29087  fressupp  32829  padct  32859  resf1o  32871  fprodeq02  32965  gsummptres2  33183  cycpmcl  33246  cycpmco2  33263  cyc3co2  33270  cycpmconjslem2  33285  cyc3conja  33287  elrspunidl  33560  lbsdiflsp0  33867  dimkerim  33868  locfinref  34082  esummono  34295  gsumesum  34300  sigaclfu2  34362  measxun2  34451  measvuni  34455  measssd  34456  pmeasmono  34565  eulerpartlemt  34612  tgoldbachgtde  34901  satfvsucsuc  35653  poimirlem9  38066  poimirlem15  38072  poimirlem25  38082  evlselv  43109  fsuppssind  43113  diophrw  43278  eldioph2lem1  43279  eldioph2lem2  43280  kelac1  43578  tfsconcatfn  43853  tfsconcatrev  43863  ioccncflimc  46397  icocncflimc  46401  dirkercncflem2  46616  dirkercncflem3  46617  sge0ss  46924  meassle  46975  meadif  46991  meaiininclem  46998  isomenndlem  47042  hspmbllem1  47138  hspmbllem2  47139  ovolval4lem1  47161  fsumsplitsndif  47913  stgrclnbgr0  48525