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

Syntax hints:   ↔ wb 205   = wceq 1539   ∖ 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 1795  ax-4 1809  ax-5 1911  ax-6 1969  ax-7 2009  ax-8 2106  ax-9 2114  ax-ext 2707

This theorem depends on definitions:  df-bi 206  df-an 398  df-or 846  df-tru 1542  df-fal 1552  df-ex 1780  df-sb 2066  df-clab 2714  df-cleq 2728  df-clel 2814  df-rab 3287  df-v 3439  df-dif 3895  df-un 3897  df-in 3899  df-ss 3909  df-nul 4263

This theorem is referenced by:  raldifeq  4430  pwundif  4563  difsnid  4749  fveqf1o  7207  f1ofvswap  7210  ralxpmap  8715  undifixp  8753  dfdom2  8799  sbthlem5  8912  sbthlem6  8913  domunsn  8952  fodomr  8953  mapdom2  8973  limensuci  8978  findcard2  8985  ssfi  8994  findcard2OLD  9100  unfiOLD  9125  marypha1lem  9236  brwdom2  9376  infdifsn  9459  ackbij1lem12  10033  ackbij1lem18  10039  ssfin4  10112  fin23lem28  10142  fin23lem30  10144  fin1a2lem13  10214  canthp1lem1  10454  xrsupss  13089  xrinfmss  13090  hashssdif  14172  hashfun  14197  hashf1lem2  14215  fsumsplit1  15502  fsumless  15553  incexclem  15593  incexc  15594  fprodsplit1f  15745  pwssplit1  20366  frlmsslss2  21027  mdetdiaglem  21792  mdetrlin  21796  mdetrsca  21797  mdetralt  21802  smadiadet  21864  isclo  22283  cmpcld  22598  rrxcph  24601  rrxdstprj1  24618  uniiccmbl  24799  itgss3  25024  dchreq  26451  axlowdimlem7  27361  axlowdimlem10  27364  undifr  30917  fressupp  31067  padct  31099  resf1o  31110  fprodeq02  31182  gsummptres2  31358  cycpmcl  31428  cycpmco2  31445  cyc3co2  31452  cycpmconjslem2  31467  cyc3conja  31469  elrspunidl  31651  lbsdiflsp0  31752  dimkerim  31753  locfinref  31836  indval2  32027  esummono  32067  gsumesum  32072  sigaclfu2  32134  measxun2  32223  measvuni  32227  measssd  32228  pmeasmono  32336  eulerpartlemt  32383  tgoldbachgtde  32685  satfvsucsuc  33372  noextendseq  33915  madeun  34111  poimirlem9  35830  poimirlem15  35836  poimirlem25  35846  fsuppssind  40319  diophrw  40618  eldioph2lem1  40619  eldioph2lem2  40620  kelac1  40926  ioccncflimc  43475  icocncflimc  43479  dirkercncflem2  43694  dirkercncflem3  43695  sge0ss  44000  meassle  44051  meadif  44067  meaiininclem  44074  isomenndlem  44118  hspmbllem1  44214  hspmbllem2  44215  ovolval4lem1  44237  fsumsplitsndif  44883