Theorem undif 4435

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

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

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 3397  df-v 3440  df-dif 3908  df-un 3910  df-in 3912  df-ss 3922  df-nul 4287

This theorem is referenced by:  undifrOLD  4437  raldifeq  4447  pwundif  4577  imadifssran  6104  fveqf1o  7243  undifixp  8868  dfdom2  8910  sbthlem5  9015  sbthlem6  9016  domunsn  9051  fodomr  9052  mapdom2  9072  limensuci  9077  findcard2  9088  ssfi  9097  fodomfir  9237  marypha1lem  9342  brwdom2  9484  infdifsn  9572  ackbij1lem12  10143  ackbij1lem18  10149  ssfin4  10223  fin23lem28  10253  fin23lem30  10255  fin1a2lem13  10325  canthp1lem1  10565  xrsupss  13229  xrinfmss  13230  hashssdif  14337  hashfun  14362  hashf1lem2  14381  fsumsplit1  15670  fsumless  15721  incexclem  15761  incexc  15762  fprodsplit1f  15915  pwssplit1  20981  frlmsslss2  21700  mdetdiaglem  22501  mdetrlin  22505  mdetrsca  22506  mdetralt  22511  smadiadet  22573  isclo  22990  cmpcld  23305  rrxcph  25308  rrxdstprj1  25325  uniiccmbl  25507  itgss3  25732  dchreq  27185  noextendseq  27595  madeun  27816  axlowdimlem7  28911  axlowdimlem10  28914  fressupp  32644  padct  32676  resf1o  32686  fprodeq02  32781  indval2  32810  gsummptres2  33019  cycpmcl  33071  cycpmco2  33088  cyc3co2  33095  cycpmconjslem2  33110  cyc3conja  33112  elrspunidl  33375  lbsdiflsp0  33598  dimkerim  33599  locfinref  33807  esummono  34020  gsumesum  34025  sigaclfu2  34087  measxun2  34176  measvuni  34180  measssd  34181  pmeasmono  34291  eulerpartlemt  34338  tgoldbachgtde  34627  satfvsucsuc  35337  poimirlem9  37608  poimirlem15  37614  poimirlem25  37624  selvvvval  42558  evlselv  42560  fsuppssind  42566  diophrw  42732  eldioph2lem1  42733  eldioph2lem2  42734  kelac1  43036  tfsconcatfn  43311  tfsconcatrev  43321  ioccncflimc  45867  icocncflimc  45871  dirkercncflem2  46086  dirkercncflem3  46087  sge0ss  46394  meassle  46445  meadif  46461  meaiininclem  46468  isomenndlem  46512  hspmbllem1  46608  hspmbllem2  46609  ovolval4lem1  46631  fsumsplitsndif  47358  stgrclnbgr0  47950