Theorem undif 4433

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 4137	. 2 ⊢ (𝐴 ⊆ 𝐵 ↔ (𝐴 ∪ 𝐵) = 𝐵)
2		undif2 4428	. . 3 ⊢ (𝐴 ∪ (𝐵 ∖ 𝐴)) = (𝐴 ∪ 𝐵)
3	2	eqeq1i 2734	. 2 ⊢ ((𝐴 ∪ (𝐵 ∖ 𝐴)) = 𝐵 ↔ (𝐴 ∪ 𝐵) = 𝐵)
4	1, 3	bitr4i 278	1 ⊢ (𝐴 ⊆ 𝐵 ↔ (𝐴 ∪ (𝐵 ∖ 𝐴)) = 𝐵)

Syntax hints:   ↔ wb 206   = wceq 1540   ∖ cdif 3900   ∪ cun 3901   ⊆ wss 3903

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-rab 3395  df-v 3438  df-dif 3906  df-un 3908  df-in 3910  df-ss 3920  df-nul 4285

This theorem is referenced by:  undifrOLD  4435  raldifeq  4445  pwundif  4575  imadifssran  6100  fveqf1o  7239  undifixp  8861  dfdom2  8903  sbthlem5  9008  sbthlem6  9009  domunsn  9044  fodomr  9045  mapdom2  9065  limensuci  9070  findcard2  9078  ssfi  9087  fodomfir  9218  marypha1lem  9323  brwdom2  9465  infdifsn  9553  ackbij1lem12  10124  ackbij1lem18  10130  ssfin4  10204  fin23lem28  10234  fin23lem30  10236  fin1a2lem13  10306  canthp1lem1  10546  xrsupss  13211  xrinfmss  13212  hashssdif  14319  hashfun  14344  hashf1lem2  14363  fsumsplit1  15652  fsumless  15703  incexclem  15743  incexc  15744  fprodsplit1f  15897  pwssplit1  20963  frlmsslss2  21682  mdetdiaglem  22483  mdetrlin  22487  mdetrsca  22488  mdetralt  22493  smadiadet  22555  isclo  22972  cmpcld  23287  rrxcph  25290  rrxdstprj1  25307  uniiccmbl  25489  itgss3  25714  dchreq  27167  noextendseq  27577  madeun  27798  axlowdimlem7  28893  axlowdimlem10  28896  fressupp  32630  padct  32662  resf1o  32673  fprodeq02  32768  indval2  32797  gsummptres2  33006  cycpmcl  33058  cycpmco2  33075  cyc3co2  33082  cycpmconjslem2  33097  cyc3conja  33099  elrspunidl  33365  lbsdiflsp0  33593  dimkerim  33594  locfinref  33808  esummono  34021  gsumesum  34026  sigaclfu2  34088  measxun2  34177  measvuni  34181  measssd  34182  pmeasmono  34292  eulerpartlemt  34339  tgoldbachgtde  34628  satfvsucsuc  35342  poimirlem9  37613  poimirlem15  37619  poimirlem25  37629  selvvvval  42562  evlselv  42564  fsuppssind  42570  diophrw  42736  eldioph2lem1  42737  eldioph2lem2  42738  kelac1  43040  tfsconcatfn  43315  tfsconcatrev  43325  ioccncflimc  45870  icocncflimc  45874  dirkercncflem2  46089  dirkercncflem3  46090  sge0ss  46397  meassle  46448  meadif  46464  meaiininclem  46471  isomenndlem  46515  hspmbllem1  46611  hspmbllem2  46612  ovolval4lem1  46634  fsumsplitsndif  47361  stgrclnbgr0  47953