Theorem undif 4505

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

Syntax hints:   ↔ wb 206   = wceq 1537   ∖ cdif 3973   ∪ cun 3974   ⊆ wss 3976

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2711

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 847  df-tru 1540  df-fal 1550  df-ex 1778  df-sb 2065  df-clab 2718  df-cleq 2732  df-clel 2819  df-rab 3444  df-v 3490  df-dif 3979  df-un 3981  df-in 3983  df-ss 3993  df-nul 4353

This theorem is referenced by:  undifrOLD  4507  raldifeq  4517  pwundif  4646  fveqf1o  7338  undifixp  8992  dfdom2  9038  sbthlem5  9153  sbthlem6  9154  domunsn  9193  fodomr  9194  mapdom2  9214  limensuci  9219  findcard2  9230  ssfi  9240  fodomfir  9396  marypha1lem  9502  brwdom2  9642  infdifsn  9726  ackbij1lem12  10299  ackbij1lem18  10305  ssfin4  10379  fin23lem28  10409  fin23lem30  10411  fin1a2lem13  10481  canthp1lem1  10721  xrsupss  13371  xrinfmss  13372  hashssdif  14461  hashfun  14486  hashf1lem2  14505  fsumsplit1  15793  fsumless  15844  incexclem  15884  incexc  15885  fprodsplit1f  16038  pwssplit1  21081  frlmsslss2  21818  mdetdiaglem  22625  mdetrlin  22629  mdetrsca  22630  mdetralt  22635  smadiadet  22697  isclo  23116  cmpcld  23431  rrxcph  25445  rrxdstprj1  25462  uniiccmbl  25644  itgss3  25870  dchreq  27320  noextendseq  27730  madeun  27940  axlowdimlem7  28981  axlowdimlem10  28984  fressupp  32700  padct  32733  resf1o  32744  fprodeq02  32827  gsummptres2  33036  cycpmcl  33109  cycpmco2  33126  cyc3co2  33133  cycpmconjslem2  33148  cyc3conja  33150  elrspunidl  33421  lbsdiflsp0  33639  dimkerim  33640  locfinref  33787  indval2  33978  esummono  34018  gsumesum  34023  sigaclfu2  34085  measxun2  34174  measvuni  34178  measssd  34179  pmeasmono  34289  eulerpartlemt  34336  tgoldbachgtde  34637  satfvsucsuc  35333  poimirlem9  37589  poimirlem15  37595  poimirlem25  37605  selvvvval  42540  evlselv  42542  fsuppssind  42548  diophrw  42715  eldioph2lem1  42716  eldioph2lem2  42717  kelac1  43020  tfsconcatfn  43300  tfsconcatrev  43310  ioccncflimc  45806  icocncflimc  45810  dirkercncflem2  46025  dirkercncflem3  46026  sge0ss  46333  meassle  46384  meadif  46400  meaiininclem  46407  isomenndlem  46451  hspmbllem1  46547  hspmbllem2  46548  ovolval4lem1  46570  fsumsplitsndif  47247